Finite Field
30 秒诊断
返回 NPA

模块

Mathlib.Data.Nat.Basic

npa-mathlib

包

2

模块

63

定理

750

声明

1016

非可信 sidecar

源文本和展示 overlay 属于展示元数据。可信证据是签名证书和 checker 结果。

定理

12

定义

0

归纳类型

0

公理

0

声明

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

哈希

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

源文本

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)