NaturalOps

📁 Source: Mathlib/SetTheory/Ordinal/NaturalOps.lean

Statistics

Metric	Count
Definitions NatOrdinal, instAdd, instAddCommMonoid, instAddMonoidWithOne, instCommSemiring, instConditionallyCompleteLinearOrderBot, instMul, instSuccAddOrder, rec, toOrdinal, «term_♯_», «term_⨳_», nadd, nmul, toNatOrdinal, instInhabitedNatOrdinal, instLinearOrderNatOrdinal, instNoMaxOrderNatOrdinal, instOneNatOrdinal, instOrderBotNatOrdinal, instSuccOrderNatOrdinal, instUncountableNatOrdinal, instWellFoundedRelationNatOrdinal, instZeroLEOneClassNatOrdinal, instZeroNatOrdinal	25
Theorems add_le_iff, bot_eq_zero, induction, instAddLeftMono, instAddLeftReflectLE, instAddLeftStrictMono, instCharZero, instIsOrderedCancelAddMonoid, instIsOrderedMonoid, instIsOrderedRing, instNeZeroOne, instWellFoundedLT, lt_add_iff, lt_mul_iff, lt_one_iff_zero, lt_wf, mul_add_lt, mul_le_iff, nmul_nadd_le, not_lt_zero, small_Icc, small_Ico, small_Iic, small_Iio, small_Ioc, small_Ioo, succ_def, toOrdinal_eq_one, toOrdinal_eq_zero, toOrdinal_max, toOrdinal_min, toOrdinal_natCast, toOrdinal_one, toOrdinal_symm_eq, toOrdinal_toNatOrdinal, toOrdinal_zero, zero_le, add_le_nadd, add_one_nmul, le_nadd_left, le_nadd_right, le_nadd_self, le_of_nadd_le_nadd_left, le_of_nadd_le_nadd_right, le_self_nadd, lt_nadd_iff, lt_nmul_iff, lt_nmul_iff₃, lt_of_nadd_lt_nadd_left, lt_of_nadd_lt_nadd_right, mul_le_nmul, nadd_assoc, nadd_comm, nadd_eq_add, nadd_le_iff, nadd_le_nadd, nadd_le_nadd_iff_left, nadd_le_nadd_iff_right, nadd_le_nadd_left, nadd_le_nadd_right, nadd_left_cancel, nadd_left_cancel_iff, nadd_left_comm, nadd_lt_nadd, nadd_lt_nadd_iff_left, nadd_lt_nadd_iff_right, nadd_lt_nadd_left, nadd_lt_nadd_of_le_of_lt, nadd_lt_nadd_of_lt_of_le, nadd_lt_nadd_right, nadd_nat, nadd_nmul, nadd_one, nadd_one_nmul, nadd_right_cancel, nadd_right_cancel_iff, nadd_right_comm, nadd_succ, nadd_zero, nat_nadd, nmul_add_one, nmul_assoc, nmul_comm, nmul_eq_mul, nmul_le_iff, nmul_le_iff₃, nmul_le_nmul, nmul_le_nmul_left, nmul_le_nmul_right, nmul_lt_nmul_of_pos_left, nmul_lt_nmul_of_pos_right, nmul_nadd, nmul_nadd_le, nmul_nadd_le₃, nmul_nadd_lt, nmul_nadd_lt₃, nmul_nadd_one, nmul_one, nmul_succ, nmul_zero, one_nadd, one_nmul, succ_nadd, succ_nmul, toNatOrdinal_eq_one, toNatOrdinal_eq_zero, toNatOrdinal_max, toNatOrdinal_min, toNatOrdinal_natCast, toNatOrdinal_one, toNatOrdinal_symm_eq, toNatOrdinal_toOrdinal, toNatOrdinal_zero, zero_nadd, zero_nmul	115
Total	140

NatOrdinal

Definitions

Name	Category	Theorems
instAdd 📖	CompOp	10 math math: instAddLeftReflectLE, lt_mul_iff, mul_add_lt, nmul_nadd_le, add_le_iff, lt_add_iff, mul_le_iff, instAddLeftStrictMono, instAddLeftMono, Ordinal.nadd_eq_add
instAddCommMonoid 📖	CompOp	1 math math: instIsOrderedCancelAddMonoid
instAddMonoidWithOne 📖	CompOp	3 math math: toOrdinal_natCast, Ordinal.toNatOrdinal_natCast, instCharZero
instCommSemiring 📖	CompOp	2 math math: instIsOrderedMonoid, instIsOrderedRing
instConditionallyCompleteLinearOrderBot 📖	CompOp	24 math math: instAddLeftReflectLE, lt_mul_iff, toOrdinal_min, instIsOrderedMonoid, instIsOrderedRing, add_le_iff, succ_def, lt_add_iff, Ordinal.toNatOrdinal_min, lt_one_iff_zero, instIsOrderedCancelAddMonoid, toOrdinal_max, not_lt_zero, mul_le_iff, instAddLeftStrictMono, instAddLeftMono, zero_le, small_Ioc, small_Iio, small_Ico, small_Ioo, small_Icc, small_Iic, Ordinal.toNatOrdinal_max
instMul 📖	CompOp	5 math math: lt_mul_iff, mul_add_lt, nmul_nadd_le, mul_le_iff, Ordinal.nmul_eq_mul
instSuccAddOrder 📖	CompOp	—
rec 📖	CompOp	—
toOrdinal 📖	CompOp	14 math math: toOrdinal_min, succ_def, toOrdinal_max, toOrdinal_natCast, toOrdinal_eq_zero, toOrdinal_symm_eq, toOrdinal_one, toOrdinal_toNatOrdinal, toOrdinal_zero, Ordinal.toNatOrdinal_toOrdinal, toOrdinal_eq_one, Ordinal.nmul_eq_mul, Ordinal.toNatOrdinal_symm_eq, Ordinal.nadd_eq_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_le_iff 📖	mathematical	—	NatOrdinal Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instAdd Preorder.toLT	—	Ordinal.nadd_le_iff
bot_eq_zero 📖	mathematical	—	Bot.bot NatOrdinal OrderBot.toBot Preorder.toLE Ordinal PartialOrder.toPreorder Ordinal.partialOrder instOrderBotNatOrdinal instZeroNatOrdinal	—	—
induction 📖	—	—	—	—	Ordinal.induction
instAddLeftMono 📖	mathematical	—	AddLeftMono NatOrdinal instAdd Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.nadd_le_nadd_left
instAddLeftReflectLE 📖	mathematical	—	AddLeftReflectLE NatOrdinal instAdd Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	LE.le.not_gt add_lt_add_right instAddLeftStrictMono
instAddLeftStrictMono 📖	mathematical	—	AddLeftStrictMono NatOrdinal instAdd Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.nadd_lt_nadd_left
instCharZero 📖	mathematical	—	CharZero NatOrdinal instAddMonoidWithOne	—	toOrdinal_natCast Ordinal.instCharZero
instIsOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid NatOrdinal instAddCommMonoid ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	add_le_add_left covariant_swap_add_of_covariant_add instAddLeftMono le_of_add_le_add_left instAddLeftReflectLE
instIsOrderedMonoid 📖	mathematical	—	IsOrderedMonoid NatOrdinal CommSemiring.toCommMonoid instCommSemiring ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.nmul_le_nmul_left Ordinal.nmul_le_nmul_right
instIsOrderedRing 📖	mathematical	—	IsOrderedRing NatOrdinal CommSemiring.toSemiring instCommSemiring ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	IsOrderedCancelAddMonoid.toIsOrderedAddMonoid instIsOrderedCancelAddMonoid MulLeftMono.toPosMulMono IsOrderedMonoid.toMulLeftMono instIsOrderedMonoid MulRightMono.toMulPosMono covariant_swap_mul_of_covariant_mul
instNeZeroOne 📖	mathematical	—	NatOrdinal instZeroNatOrdinal instOneNatOrdinal	—	Ordinal.instNeZeroOne
instWellFoundedLT 📖	mathematical	—	WellFoundedLT NatOrdinal Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal	—	Ordinal.wellFoundedLT
lt_add_iff 📖	mathematical	—	NatOrdinal Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instAdd Preorder.toLE	—	Ordinal.lt_nadd_iff
lt_mul_iff 📖	mathematical	—	NatOrdinal Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instMul Preorder.toLE instAdd	—	Ordinal.lt_nmul_iff
lt_one_iff_zero 📖	mathematical	—	NatOrdinal Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instOneNatOrdinal instZeroNatOrdinal	—	Ordinal.lt_one_iff_zero
lt_wf 📖	mathematical	—	NatOrdinal Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal	—	Ordinal.lt_wf
mul_add_lt 📖	mathematical	NatOrdinal Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	instAdd instMul	—	Ordinal.nmul_nadd_lt
mul_le_iff 📖	mathematical	—	NatOrdinal Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instMul Preorder.toLT instAdd	—	Ordinal.nmul_le_iff
nmul_nadd_le 📖	mathematical	NatOrdinal Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	instAdd instMul	—	Ordinal.nmul_nadd_le
not_lt_zero 📖	mathematical	—	NatOrdinal Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNatOrdinal	—	not_lt_zero Ordinal.canonicallyOrderedAdd
small_Icc 📖	mathematical	—	Small Set.Elem NatOrdinal Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Icc
small_Ico 📖	mathematical	—	Small Set.Elem NatOrdinal Set.Ico PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Ico
small_Iic 📖	mathematical	—	Small Set.Elem NatOrdinal Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Iic
small_Iio 📖	mathematical	—	Small Set.Elem NatOrdinal Set.Iio PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Iio
small_Ioc 📖	mathematical	—	Small Set.Elem NatOrdinal Set.Ioc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Ioc
small_Ioo 📖	mathematical	—	Small Set.Elem NatOrdinal Set.Ioo PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.small_Ioo
succ_def 📖	mathematical	—	Order.succ NatOrdinal PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instSuccOrderNatOrdinal DFunLike.coe OrderIso Ordinal Preorder.toLE Ordinal.partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso Ordinal.toNatOrdinal Ordinal.add toOrdinal Ordinal.one	—	—
toOrdinal_eq_one 📖	mathematical	—	DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal Ordinal.partialOrder instFunLikeOrderIso toOrdinal Ordinal.one instOneNatOrdinal	—	—
toOrdinal_eq_zero 📖	mathematical	—	DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal Ordinal.partialOrder instFunLikeOrderIso toOrdinal Ordinal.zero instZeroNatOrdinal	—	—
toOrdinal_max 📖	mathematical	—	DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal Ordinal.partialOrder instFunLikeOrderIso toOrdinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Ordinal.instConditionallyCompleteLinearOrderBot	—	—
toOrdinal_min 📖	mathematical	—	DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal Ordinal.partialOrder instFunLikeOrderIso toOrdinal SemilatticeInf.toMin ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Ordinal.instConditionallyCompleteLinearOrderBot	—	—
toOrdinal_natCast 📖	mathematical	—	DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal Ordinal.partialOrder instFunLikeOrderIso toOrdinal AddMonoidWithOne.toNatCast instAddMonoidWithOne Ordinal.addMonoidWithOne	—	Ordinal.nadd_one
toOrdinal_one 📖	mathematical	—	DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal Ordinal.partialOrder instFunLikeOrderIso toOrdinal instOneNatOrdinal Ordinal.one	—	—
toOrdinal_symm_eq 📖	mathematical	—	OrderIso.symm NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal Ordinal.partialOrder toOrdinal Ordinal.toNatOrdinal	—	—
toOrdinal_toNatOrdinal 📖	mathematical	—	DFunLike.coe OrderIso Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso Ordinal.toNatOrdinal toOrdinal	—	—
toOrdinal_zero 📖	mathematical	—	DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal Ordinal.partialOrder instFunLikeOrderIso toOrdinal instZeroNatOrdinal Ordinal.zero	—	—
zero_le 📖	mathematical	—	NatOrdinal Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNatOrdinal	—	zero_le Ordinal.canonicallyOrderedAdd

NaturalOps

Definitions

Name	Category	Theorems
«term_♯_» 📖	CompOp	—
«term_⨳_» 📖	CompOp	—

Ordinal

Definitions

Name	Category	Theorems
nadd 📖	CompOp	56 math math: succ_nmul, zero_nadd, SetTheory.Game.birthday_add_le, nmul_le_iff₃, SetTheory.PGame.birthday_add, nadd_le_nadd, nadd_one_nmul, SetTheory.Game.birthday_sub_le, nmul_add_one, nadd_le_nadd_iff_right, nat_nadd, nmul_nadd_one, nadd_le_nadd_iff_left, SetTheory.PGame.birthday_sub, le_nadd_self, nmul_succ, nmul_nadd_le, nadd_left_comm, nadd_assoc, lt_nmul_iff₃, lt_nmul_iff, le_self_nadd, nmul_nadd_le₃, nadd_right_cancel_iff, nadd_lt_nadd_of_le_of_lt, le_nadd_left, nadd_le_iff, add_le_nadd, one_nadd, nmul_nadd, nadd_comm, nadd_lt_nadd_right, nadd_left_cancel_iff, nadd_nat, nadd_right_comm, nadd_le_nadd_right, nadd_succ, nmul_nadd_lt, nadd_nmul, le_nadd_right, nadd_zero, nadd_lt_nadd_left, nmul_nadd_lt₃, toPGame_nadd, nadd_lt_nadd_iff_right, nadd_lt_nadd_of_lt_of_le, nmul_le_iff, lt_nadd_iff, succ_nadd, nadd_one, toGame_nadd, nadd_le_nadd_left, add_one_nmul, nadd_lt_nadd_iff_left, nadd_eq_add, nadd_lt_nadd
nmul 📖	CompOp	31 math math: succ_nmul, nmul_le_iff₃, one_nmul, mul_le_nmul, nadd_one_nmul, nmul_add_one, nmul_comm, toPGame_nmul, nmul_lt_nmul_of_pos_right, nmul_nadd_one, nmul_succ, nmul_nadd_le, lt_nmul_iff₃, lt_nmul_iff, nmul_nadd_le₃, nmul_lt_nmul_of_pos_left, nmul_zero, nmul_nadd, zero_nmul, toGame_nmul, nmul_assoc, nmul_one, nmul_nadd_lt, nadd_nmul, nmul_nadd_lt₃, nmul_le_nmul, nmul_le_nmul_right, nmul_le_iff, nmul_eq_mul, add_one_nmul, nmul_le_nmul_left
toNatOrdinal 📖	CompOp	14 math math: toNatOrdinal_eq_one, NatOrdinal.succ_def, toNatOrdinal_min, toNatOrdinal_one, toNatOrdinal_zero, toNatOrdinal_eq_zero, toNatOrdinal_natCast, NatOrdinal.toOrdinal_symm_eq, NatOrdinal.toOrdinal_toNatOrdinal, toNatOrdinal_toOrdinal, nmul_eq_mul, toNatOrdinal_max, toNatOrdinal_symm_eq, nadd_eq_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_le_nadd 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder add nadd	—	add_zero nadd_zero add_succ nadd_succ Order.succ_le_succ_iff instNoMaxOrder Order.IsNormal.apply_of_isSuccLimit isNormal_add_right iSup_le_iff small_Iio LE.le.trans nadd_le_nadd_left LT.lt.le
add_one_nmul 📖	mathematical	—	nmul Ordinal add one nadd	—	succ_nmul
le_nadd_left 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nadd	—	LE.le.trans le_nadd_self nadd_le_nadd_left
le_nadd_right 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nadd	—	LE.le.trans le_self_nadd nadd_le_nadd_right
le_nadd_self 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nadd	—	zero_nadd nadd_le_nadd_right zero_le canonicallyOrderedAdd
le_of_nadd_le_nadd_left 📖	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nadd	—	—	le_of_add_le_add_left NatOrdinal.instAddLeftReflectLE
le_of_nadd_le_nadd_right 📖	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nadd	—	—	le_of_add_le_add_right IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le NatOrdinal.instAddLeftMono
le_self_nadd 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nadd	—	nadd_zero nadd_le_nadd_left zero_le canonicallyOrderedAdd
lt_nadd_iff 📖	mathematical	—	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder nadd Preorder.toLE	—	nadd.eq_1 small_Iio instNoMaxOrder
lt_nmul_iff 📖	mathematical	—	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder nmul Preorder.toLE nadd	—	notMem_of_lt_csInf nmul.eq_1 bot_le LE.le.trans_lt nmul_nadd_lt nadd_lt_nadd_iff_right
lt_nmul_iff₃ 📖	mathematical	—	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder nmul Preorder.toLE nadd	—	lt_nmul_iff nadd_le_nadd nmul_nadd_le LT.lt.le nadd_assoc nadd_left_comm nadd_le_nadd_iff_left nadd_nmul LE.le.trans_lt nmul_nadd_lt₃ nadd_lt_nadd_iff_right
lt_of_nadd_lt_nadd_left 📖	—	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder nadd	—	—	lt_of_add_lt_add_left contravariant_lt_of_covariant_le NatOrdinal.instAddLeftMono
lt_of_nadd_lt_nadd_right 📖	—	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder nadd	—	—	lt_of_add_lt_add_right contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le NatOrdinal.instAddLeftMono
mul_le_nmul 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass monoidWithZero nmul	—	MulZeroClass.mul_zero nmul_zero mul_succ nmul_succ LE.le.trans add_le_nadd nadd_le_nadd_right eq_zero_or_pos canonicallyOrderedAdd MulZeroClass.zero_mul zero_nmul Order.IsNormal.apply_of_isSuccLimit isNormal_mul_right iSup_le_iff small_Iio le_imp_le_of_le_of_le le_refl nmul_le_nmul le_of_lt
nadd_assoc 📖	mathematical	—	nadd	—	—
nadd_comm 📖	mathematical	—	nadd	—	—
nadd_eq_add 📖	mathematical	—	nadd DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal partialOrder instFunLikeOrderIso NatOrdinal.toOrdinal NatOrdinal.instAdd toNatOrdinal	—	—
nadd_le_iff 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nadd Preorder.toLT	—	not_lt lt_nadd_iff
nadd_le_nadd 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nadd	—	add_le_add NatOrdinal.instAddLeftMono covariant_swap_add_of_covariant_add
nadd_le_nadd_iff_left 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nadd	—	add_le_add_iff_left NatOrdinal.instAddLeftMono NatOrdinal.instAddLeftReflectLE
nadd_le_nadd_iff_right 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nadd	—	add_le_add_iff_right covariant_swap_add_of_covariant_add NatOrdinal.instAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
nadd_le_nadd_left 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nadd	—	lt_or_eq_of_le LT.lt.le nadd_lt_nadd_left le_rfl
nadd_le_nadd_right 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nadd	—	lt_or_eq_of_le LT.lt.le nadd_lt_nadd_right le_rfl
nadd_left_cancel 📖	—	nadd	—	—	add_left_cancel IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid
nadd_left_cancel_iff 📖	mathematical	—	nadd	—	add_left_cancel_iff IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid
nadd_left_comm 📖	mathematical	—	nadd	—	add_left_comm
nadd_lt_nadd 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder	nadd	—	add_lt_add NatOrdinal.instAddLeftStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid covariant_swap_add_of_covariant_add NatOrdinal.instAddLeftMono
nadd_lt_nadd_iff_left 📖	mathematical	—	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder nadd	—	add_lt_add_iff_left NatOrdinal.instAddLeftStrictMono contravariant_lt_of_covariant_le NatOrdinal.instAddLeftMono
nadd_lt_nadd_iff_right 📖	mathematical	—	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder nadd	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid covariant_swap_add_of_covariant_add NatOrdinal.instAddLeftMono contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
nadd_lt_nadd_left 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder	nadd	—	lt_nadd_iff le_rfl
nadd_lt_nadd_of_le_of_lt 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder Preorder.toLT	nadd	—	add_lt_add_of_le_of_lt NatOrdinal.instAddLeftStrictMono covariant_swap_add_of_covariant_add NatOrdinal.instAddLeftMono
nadd_lt_nadd_of_lt_of_le 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder Preorder.toLE	nadd	—	add_lt_add_of_lt_of_le NatOrdinal.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid covariant_swap_add_of_covariant_add
nadd_lt_nadd_right 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder	nadd	—	lt_nadd_iff le_rfl
nadd_nat 📖	mathematical	—	nadd Ordinal AddMonoidWithOne.toNatCast addMonoidWithOne add	—	Nat.cast_zero nadd_zero add_zero Nat.cast_succ add_one_eq_succ nadd_succ add_succ
nadd_nmul 📖	mathematical	—	nmul nadd	—	nmul_comm nmul_nadd
nadd_one 📖	mathematical	—	nadd Ordinal one Order.succ PartialOrder.toPreorder partialOrder instSuccOrder	—	nadd.eq_1 ciSup_unique zero_lt_one' instZeroLEOneClass instNeZeroOne Iio_one_default_eq nadd_zero max_eq_right_iff iSup_le_iff small_Iio Order.succ_le_succ_iff instNoMaxOrder Order.succ_le_iff
nadd_one_nmul 📖	mathematical	—	nmul nadd Ordinal one	—	add_one_mul Distrib.rightDistribClass
nadd_right_cancel 📖	—	nadd	—	—	add_right_cancel IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid
nadd_right_cancel_iff 📖	mathematical	—	nadd	—	add_right_cancel_iff IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd NatOrdinal.instIsOrderedCancelAddMonoid
nadd_right_comm 📖	mathematical	—	nadd	—	add_right_comm
nadd_succ 📖	mathematical	—	nadd Order.succ Ordinal PartialOrder.toPreorder partialOrder instSuccOrder	—	nadd_one nadd_assoc
nadd_zero 📖	mathematical	—	nadd Ordinal zero	—	nadd.eq_1 ciSup_of_empty instIsEmptyIioZero sup_bot_eq iSup_succ
nat_nadd 📖	mathematical	—	nadd Ordinal AddMonoidWithOne.toNatCast addMonoidWithOne add	—	nadd_comm nadd_nat
nmul_add_one 📖	mathematical	—	nmul Ordinal add one nadd	—	nmul_succ
nmul_assoc 📖	mathematical	—	nmul	—	—
nmul_comm 📖	mathematical	—	nmul	—	—
nmul_eq_mul 📖	mathematical	—	nmul DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal partialOrder instFunLikeOrderIso NatOrdinal.toOrdinal NatOrdinal.instMul toNatOrdinal	—	—
nmul_le_iff 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nmul Preorder.toLT nadd	—	not_iff_not
nmul_le_iff₃ 📖	mathematical	—	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder nmul Preorder.toLT nadd	—	Iff.not lt_nmul_iff₃
nmul_le_nmul 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nmul	—	LE.le.trans nmul_le_nmul_left nmul_le_nmul_right
nmul_le_nmul_left 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nmul	—	nmul_comm nmul_le_nmul_right
nmul_le_nmul_right 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nmul	—	lt_or_eq_of_le eq_zero_or_pos canonicallyOrderedAdd LT.lt.le nmul_lt_nmul_of_pos_left zero_nmul
nmul_lt_nmul_of_pos_left 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder zero	nmul	—	lt_nmul_iff zero_nmul nadd_zero zero_nadd
nmul_lt_nmul_of_pos_right 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder zero	nmul	—	lt_nmul_iff nmul_zero nadd_zero
nmul_nadd 📖	mathematical	—	nmul nadd	—	—
nmul_nadd_le 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nadd nmul	—	lt_or_eq_of_le LT.lt.le nmul_nadd_lt nadd_comm le_refl le_rfl
nmul_nadd_le₃ 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder partialOrder	nadd nmul	—	nadd_nmul nmul_nadd_le
nmul_nadd_lt 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder	nadd nmul	—	nmul.eq_1 csInf_mem wellFoundedLT
nmul_nadd_lt₃ 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder	nadd nmul	—	nadd_nmul nmul_nadd_lt
nmul_nadd_one 📖	mathematical	—	nmul nadd Ordinal one	—	mul_add_one Distrib.leftDistribClass
nmul_one 📖	mathematical	—	nmul Ordinal one	—	nmul.eq_1 Set.ext le_of_forall_lt nmul_zero nadd_zero LT.lt.trans_le csInf_Ici
nmul_succ 📖	mathematical	—	nmul Order.succ Ordinal PartialOrder.toPreorder partialOrder instSuccOrder nadd	—	nadd_one nmul_nadd_one
nmul_zero 📖	mathematical	—	nmul Ordinal zero	—	canonicallyOrderedAdd zero_nadd instIsEmptyFalse
one_nadd 📖	mathematical	—	nadd Ordinal one Order.succ PartialOrder.toPreorder partialOrder instSuccOrder	—	nadd_comm nadd_one
one_nmul 📖	mathematical	—	nmul Ordinal one	—	nmul_comm nmul_one
succ_nadd 📖	mathematical	—	nadd Order.succ Ordinal PartialOrder.toPreorder partialOrder instSuccOrder	—	one_nadd nadd_assoc
succ_nmul 📖	mathematical	—	nmul Order.succ Ordinal PartialOrder.toPreorder partialOrder instSuccOrder nadd	—	nadd_one nadd_one_nmul
toNatOrdinal_eq_one 📖	mathematical	—	DFunLike.coe OrderIso Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso toNatOrdinal instOneNatOrdinal one	—	—
toNatOrdinal_eq_zero 📖	mathematical	—	DFunLike.coe OrderIso Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso toNatOrdinal instZeroNatOrdinal zero	—	—
toNatOrdinal_max 📖	mathematical	—	DFunLike.coe OrderIso Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso toNatOrdinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot NatOrdinal.instConditionallyCompleteLinearOrderBot	—	—
toNatOrdinal_min 📖	mathematical	—	DFunLike.coe OrderIso Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso toNatOrdinal SemilatticeInf.toMin ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot NatOrdinal.instConditionallyCompleteLinearOrderBot	—	—
toNatOrdinal_natCast 📖	mathematical	—	DFunLike.coe OrderIso Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso toNatOrdinal AddMonoidWithOne.toNatCast addMonoidWithOne NatOrdinal.instAddMonoidWithOne	—	NatOrdinal.toOrdinal_natCast
toNatOrdinal_one 📖	mathematical	—	DFunLike.coe OrderIso Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso toNatOrdinal one instOneNatOrdinal	—	—
toNatOrdinal_symm_eq 📖	mathematical	—	OrderIso.symm Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal toNatOrdinal NatOrdinal.toOrdinal	—	—
toNatOrdinal_toOrdinal 📖	mathematical	—	DFunLike.coe OrderIso NatOrdinal Ordinal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal partialOrder instFunLikeOrderIso NatOrdinal.toOrdinal toNatOrdinal	—	—
toNatOrdinal_zero 📖	mathematical	—	DFunLike.coe OrderIso Ordinal NatOrdinal Preorder.toLE PartialOrder.toPreorder partialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNatOrdinal instFunLikeOrderIso toNatOrdinal zero instZeroNatOrdinal	—	—
zero_nadd 📖	mathematical	—	nadd Ordinal zero	—	nadd_comm nadd_zero
zero_nmul 📖	mathematical	—	nmul Ordinal zero	—	nmul_comm nmul_zero

(root)

Definitions

Name	Category	Theorems
NatOrdinal 📖	CompOp	45 math math: NatOrdinal.instAddLeftReflectLE, NatOrdinal.lt_mul_iff, Ordinal.toNatOrdinal_eq_one, NatOrdinal.toOrdinal_min, NatOrdinal.instIsOrderedMonoid, NatOrdinal.instIsOrderedRing, NatOrdinal.add_le_iff, NatOrdinal.succ_def, NatOrdinal.lt_add_iff, NatOrdinal.bot_eq_zero, Ordinal.toNatOrdinal_min, NatOrdinal.lt_one_iff_zero, NatOrdinal.instIsOrderedCancelAddMonoid, NatOrdinal.toOrdinal_max, NatOrdinal.not_lt_zero, Ordinal.toNatOrdinal_one, NatOrdinal.instNeZeroOne, NatOrdinal.mul_le_iff, NatOrdinal.toOrdinal_natCast, NatOrdinal.instAddLeftStrictMono, NatOrdinal.instAddLeftMono, Ordinal.toNatOrdinal_zero, NatOrdinal.toOrdinal_eq_zero, Ordinal.toNatOrdinal_eq_zero, NatOrdinal.zero_le, Ordinal.toNatOrdinal_natCast, NatOrdinal.toOrdinal_symm_eq, NatOrdinal.toOrdinal_one, NatOrdinal.toOrdinal_toNatOrdinal, NatOrdinal.instWellFoundedLT, NatOrdinal.small_Ioc, NatOrdinal.small_Iio, NatOrdinal.small_Ico, NatOrdinal.small_Ioo, NatOrdinal.toOrdinal_zero, NatOrdinal.small_Icc, Ordinal.toNatOrdinal_toOrdinal, NatOrdinal.toOrdinal_eq_one, Ordinal.nmul_eq_mul, NatOrdinal.small_Iic, NatOrdinal.instCharZero, Ordinal.toNatOrdinal_max, Ordinal.toNatOrdinal_symm_eq, Ordinal.nadd_eq_add, NatOrdinal.lt_wf
instInhabitedNatOrdinal 📖	CompOp	—
instLinearOrderNatOrdinal 📖	CompOp	23 math math: Ordinal.toNatOrdinal_eq_one, NatOrdinal.toOrdinal_min, NatOrdinal.succ_def, Ordinal.toNatOrdinal_min, NatOrdinal.toOrdinal_max, Ordinal.toNatOrdinal_one, NatOrdinal.toOrdinal_natCast, Ordinal.toNatOrdinal_zero, NatOrdinal.toOrdinal_eq_zero, Ordinal.toNatOrdinal_eq_zero, Ordinal.toNatOrdinal_natCast, NatOrdinal.toOrdinal_symm_eq, NatOrdinal.toOrdinal_one, NatOrdinal.toOrdinal_toNatOrdinal, NatOrdinal.instWellFoundedLT, NatOrdinal.toOrdinal_zero, Ordinal.toNatOrdinal_toOrdinal, NatOrdinal.toOrdinal_eq_one, Ordinal.nmul_eq_mul, Ordinal.toNatOrdinal_max, Ordinal.toNatOrdinal_symm_eq, Ordinal.nadd_eq_add, NatOrdinal.lt_wf
instNoMaxOrderNatOrdinal 📖	CompOp	—
instOneNatOrdinal 📖	CompOp	6 math math: Ordinal.toNatOrdinal_eq_one, NatOrdinal.lt_one_iff_zero, Ordinal.toNatOrdinal_one, NatOrdinal.instNeZeroOne, NatOrdinal.toOrdinal_one, NatOrdinal.toOrdinal_eq_one
instOrderBotNatOrdinal 📖	CompOp	1 math math: NatOrdinal.bot_eq_zero
instSuccOrderNatOrdinal 📖	CompOp	1 math math: NatOrdinal.succ_def
instUncountableNatOrdinal 📖	CompOp	—
instWellFoundedRelationNatOrdinal 📖	CompOp	—
instZeroLEOneClassNatOrdinal 📖	CompOp	—
instZeroNatOrdinal 📖	CompOp	9 math math: NatOrdinal.bot_eq_zero, NatOrdinal.lt_one_iff_zero, NatOrdinal.not_lt_zero, NatOrdinal.instNeZeroOne, Ordinal.toNatOrdinal_zero, NatOrdinal.toOrdinal_eq_zero, Ordinal.toNatOrdinal_eq_zero, NatOrdinal.zero_le, NatOrdinal.toOrdinal_zero

---

← Back to Index