Finite Field
30秒診断
NPAへ戻る

Module

Mathlib.Data.Nat.Basic

npa-mathlib

Packages

2

Module

63

Theorem

750

Declarations

1016

信頼境界外の sidecar

Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。

Theorem

12

Definition

0

Inductive type

0

Axiom

0

Declarations

nat_zero_self_eq

@Eq.{1} Nat Nat.zero Nat.zero

theorem

nat_succ_zero_self_eq

@Eq.{1} Nat (Nat.succ Nat.zero) (Nat.succ Nat.zero)

theorem

nat_id

forall (n : Nat), Nat

theorem

nat_const_zero

forall (n : Nat), Nat

theorem

nat_apply_fn

forall (f : forall (n : Nat), Nat), forall (n : Nat), Nat

theorem

nat_const_succ_zero

forall (n : Nat), Nat

theorem

nat_apply_twice

forall (f : forall (n : Nat), Nat), forall (n : Nat), Nat

theorem

nat_compose

forall (f : forall (n : Nat), Nat), forall (g : forall (n : Nat), Nat), forall (n : Nat), Nat

theorem

nat_ignore_middle

forall (x : Nat), forall (y : Nat), forall (z : Nat), Nat

theorem

nat_select_middle

forall (x : Nat), forall (y : Nat), forall (z : Nat), Nat

theorem

nat_select_last

forall (x : Nat), forall (y : Nat), forall (z : Nat), Nat

theorem

nat_succ_self_eq

forall (n : Nat), @Eq.{1} Nat (Nat.succ n) (Nat.succ n)

theorem

Hashes

source
sha256:f899f8fcded51dfeef0f37960bb6050d50de22e134e076b6f44805d939bea8cd
certificateFile
sha256:d60f3e74b958bcd3896df5226816de079a5673b65f6cdc6489760305bbb982ec
export
sha256:9fc6d82aad7043992d726def9add7c2bf1b81c529923ee28143f6127d3ea5f13
axiomReport
sha256:7715c06c634de0020345067c58ecf3bd23c10e71d84f4b97cd4c2e00e82c1a07
certificate
sha256:e01b724ffa5ccb171b673f8431716ac42f846d6b70cbee0e59c5216775fa5cc4

Source

import Std.Logic.Eq
import Std.Nat.Basic

theorem nat_zero_self_eq :
  @Eq.{1} Nat Nat.zero Nat.zero :=
  @Eq.refl.{1} Nat Nat.zero

theorem nat_succ_zero_self_eq :
  @Eq.{1} Nat (Nat.succ Nat.zero) (Nat.succ Nat.zero) :=
  @Eq.refl.{1} Nat (Nat.succ Nat.zero)

theorem nat_id :
  forall (n : Nat), Nat :=
  fun n => n

theorem nat_const_zero :
  forall (n : Nat), Nat :=
  fun n => Nat.zero

theorem nat_apply_fn :
  forall (f : forall (n : Nat), Nat), forall (n : Nat), Nat :=
  fun f => fun n => f n

theorem nat_const_succ_zero :
  forall (n : Nat), Nat :=
  fun n => Nat.succ Nat.zero

theorem nat_apply_twice :
  forall (f : forall (n : Nat), Nat), forall (n : Nat), Nat :=
  fun f => fun n => f (f n)

theorem nat_compose :
  forall (f : forall (n : Nat), Nat), forall (g : forall (n : Nat), Nat), forall (n : Nat), Nat :=
  fun f => fun g => fun n => f (g n)

theorem nat_ignore_middle :
  forall (x : Nat), forall (y : Nat), forall (z : Nat), Nat :=
  fun x => fun y => fun z => x

theorem nat_select_middle :
  forall (x : Nat), forall (y : Nat), forall (z : Nat), Nat :=
  fun x => fun y => fun z => y

theorem nat_select_last :
  forall (x : Nat), forall (y : Nat), forall (z : Nat), Nat :=
  fun x => fun y => fun z => z

theorem nat_succ_self_eq :
  forall (n : Nat), @Eq.{1} Nat (Nat.succ n) (Nat.succ n) :=
  fun n => @Eq.refl.{1} Nat (Nat.succ n)