Nim

📁 Source: Mathlib/SetTheory/Game/Nim.lean

Statistics

Metric	Count
Definitions `grundyValue`, `leftMovesNimRecOn`, `nim`, `nimOneRelabelling`, `nimZeroRelabelling`, `rightMovesNimRecOn`, `toLeftMovesNim`, `toRightMovesNim`, `uniqueNimOneLeftMoves`, `uniqueNimOneRightMoves`	10
Theorems `default_nim_one_leftMoves_eq`, `default_nim_one_rightMoves_eq`, `equiv_nim_grundyValue`, `exists_grundyValue_moveLeft_of_lt`, `exists_grundyValue_moveRight_of_lt`, `grundyValue_add`, `grundyValue_eq_iff_equiv`, `grundyValue_eq_iff_equiv_nim`, `grundyValue_eq_sInf_moveLeft`, `grundyValue_eq_sInf_moveRight`, `grundyValue_iff_equiv_zero`, `grundyValue_le_of_forall_moveLeft`, `grundyValue_le_of_forall_moveRight`, `grundyValue_ne_moveLeft`, `grundyValue_ne_moveRight`, `grundyValue_neg`, `grundyValue_nim_add_nim`, `grundyValue_star`, `grundyValue_zero`, `impartial_nim`, `isEmpty_nim_zero_leftMoves`, `isEmpty_nim_zero_rightMoves`, `le_grundyValue_of_Iio_subset_moveLeft`, `le_grundyValue_of_Iio_subset_moveRight`, `leftMoves_nim`, `moveLeft_nim`, `moveLeft_nim_heq`, `moveLeft_toLeftMovesNim`, `moveRight_nim`, `moveRight_nim_heq`, `moveRight_toRightMovesNim`, `neg_nim`, `nim_add_equiv_zero_iff`, `nim_add_fuzzy_zero_iff`, `nim_add_nim_equiv`, `nim_birthday`, `nim_equiv_iff_eq`, `nim_fuzzy_zero_of_ne_zero`, `nim_grundyValue`, `nim_one_equiv`, `nim_one_moveLeft`, `nim_one_moveRight`, `nim_zero_equiv`, `rightMoves_nim`, `toLeftMovesNim_one_symm`, `toLeftMovesNim_symm_lt`, `toRightMovesNim_one_symm`, `toRightMovesNim_symm_lt`	48
Total	58

SetTheory.PGame

Definitions

Name	Category	Theorems
`grundyValue` 📖	CompOp	14 math math: `grundyValue_eq_sInf_moveLeft`, `grundyValue_eq_iff_equiv_nim`, `grundyValue_nim_add_nim`, `grundyValue_eq_iff_equiv`, `grundyValue_zero`, `grundyValue_eq_sInf_moveRight`, `grundyValue_le_of_forall_moveLeft`, `grundyValue_star`, `equiv_nim_grundyValue`, `grundyValue_neg`, `nim_grundyValue`, `grundyValue_le_of_forall_moveRight`, `grundyValue_iff_equiv_zero`, `grundyValue_add`
`leftMovesNimRecOn` 📖	CompOp	—
`nim` 📖	CompOp	32 math math: `nim_add_equiv_zero_iff`, `default_nim_one_rightMoves_eq`, `impartial_nim`, `grundyValue_eq_iff_equiv_nim`, `grundyValue_nim_add_nim`, `isEmpty_nim_zero_leftMoves`, `nim_one_equiv`, `toRightMovesNim_one_symm`, `nim_fuzzy_zero_of_ne_zero`, `moveRight_nim`, `nim_one_moveLeft`, `default_nim_one_leftMoves_eq`, `equiv_nim_grundyValue`, `nim_add_fuzzy_zero_iff`, `rightMoves_nim`, `nim_zero_equiv`, `leftMoves_nim`, `toLeftMovesNim_symm_lt`, `nim_equiv_iff_eq`, `moveLeft_toLeftMovesNim`, `nim_birthday`, `nim_one_moveRight`, `nim_grundyValue`, `moveRight_nim_heq`, `neg_nim`, `moveLeft_nim_heq`, `moveLeft_nim`, `nim_add_nim_equiv`, `moveRight_toRightMovesNim`, `isEmpty_nim_zero_rightMoves`, `toRightMovesNim_symm_lt`, `toLeftMovesNim_one_symm`
`nimOneRelabelling` 📖	CompOp	—
`nimZeroRelabelling` 📖	CompOp	—
`rightMovesNimRecOn` 📖	CompOp	—
`toLeftMovesNim` 📖	CompOp	5 math math: `default_nim_one_leftMoves_eq`, `toLeftMovesNim_symm_lt`, `moveLeft_toLeftMovesNim`, `moveLeft_nim`, `toLeftMovesNim_one_symm`
`toRightMovesNim` 📖	CompOp	5 math math: `default_nim_one_rightMoves_eq`, `toRightMovesNim_one_symm`, `moveRight_nim`, `moveRight_toRightMovesNim`, `toRightMovesNim_symm_lt`
`uniqueNimOneLeftMoves` 📖	CompOp	1 math math: `default_nim_one_leftMoves_eq`
`uniqueNimOneRightMoves` 📖	CompOp	1 math math: `default_nim_one_rightMoves_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`default_nim_one_leftMoves_eq` 📖	mathematical	—	`LeftMoves` `nim` `Ordinal` `Ordinal.one` `Unique.instInhabited` `uniqueNimOneLeftMoves` `DFunLike.coe` `Equiv` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLeftMovesNim` `Set` `Set.instMembership` `Ordinal.zero` `Preorder.toLT` `Set.mem_Iio` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne`	—	—
`default_nim_one_rightMoves_eq` 📖	mathematical	—	`RightMoves` `nim` `Ordinal` `Ordinal.one` `Unique.instInhabited` `uniqueNimOneRightMoves` `DFunLike.coe` `Equiv` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `toRightMovesNim` `Set` `Set.instMembership` `Ordinal.zero` `Preorder.toLT` `Set.mem_Iio` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne`	—	—
`equiv_nim_grundyValue` 📖	mathematical	—	`SetTheory.PGame` `setoid` `nim` `DFunLike.coe` `OrderIso` `Nimber` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nimber.instLinearOrder` `Ordinal.partialOrder` `instFunLikeOrderIso` `Nimber.toOrdinal` `grundyValue`	—	—
`exists_grundyValue_moveLeft_of_lt` 📖	mathematical	`Nimber` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Nimber.instConditionallyCompleteLinearOrderBot` `grundyValue`	`moveLeft`	—	`LT.lt.not_ge` `grundyValue_eq_sInf_moveLeft` `csInf_le'`
`exists_grundyValue_moveRight_of_lt` 📖	mathematical	`Nimber` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Nimber.instConditionallyCompleteLinearOrderBot` `grundyValue`	`moveRight`	—	`exists_grundyValue_moveLeft_of_lt` `grundyValue_neg` `Impartial.moveRight_impartial` `moveLeft_neg`
`grundyValue_add` 📖	mathematical	—	`grundyValue` `SetTheory.PGame` `instAdd` `Nimber` `Nimber.instAdd`	—	`Nimber.toOrdinal_toNimber` `grundyValue_nim_add_nim` `grundyValue_eq_iff_equiv` `Impartial.impartial_add` `impartial_nim` `add_congr` `equiv_nim_grundyValue`
`grundyValue_eq_iff_equiv` 📖	mathematical	—	`grundyValue` `SetTheory.PGame` `setoid`	—	`grundyValue_eq_iff_equiv_nim` `equiv_congr_left` `equiv_nim_grundyValue`
`grundyValue_eq_iff_equiv_nim` 📖	mathematical	—	`grundyValue` `SetTheory.PGame` `setoid` `nim` `DFunLike.coe` `OrderIso` `Nimber` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nimber.instLinearOrder` `Ordinal.partialOrder` `instFunLikeOrderIso` `Nimber.toOrdinal`	—	`equiv_nim_grundyValue` `nim_equiv_iff_eq` `Equiv.trans` `Equiv.symm`
`grundyValue_eq_sInf_moveLeft` 📖	mathematical	—	`grundyValue` `InfSet.sInf` `Nimber` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Nimber.instConditionallyCompleteLinearOrderBot` `Compl.compl` `Set` `Set.instCompl` `Set.range` `LeftMoves` `SetTheory.PGame` `moveLeft`	—	`grundyValue.eq_1`
`grundyValue_eq_sInf_moveRight` 📖	mathematical	—	`grundyValue` `InfSet.sInf` `Nimber` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Nimber.instConditionallyCompleteLinearOrderBot` `Compl.compl` `Set` `Set.instCompl` `Set.range` `RightMoves` `SetTheory.PGame` `moveRight`	—	`grundyValue_neg` `grundyValue_eq_sInf_moveLeft` `Impartial.moveRight_impartial`
`grundyValue_iff_equiv_zero` 📖	mathematical	—	`grundyValue` `Nimber` `instZeroNimber` `SetTheory.PGame` `setoid` `instZero`	—	`grundyValue_eq_iff_equiv` `Impartial.impartial_zero` `grundyValue_zero`
`grundyValue_le_of_forall_moveLeft` 📖	mathematical	—	`Nimber` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Nimber.instConditionallyCompleteLinearOrderBot` `grundyValue`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `exists_grundyValue_moveLeft_of_lt`
`grundyValue_le_of_forall_moveRight` 📖	mathematical	—	`Nimber` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Nimber.instConditionallyCompleteLinearOrderBot` `grundyValue`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `exists_grundyValue_moveRight_of_lt`
`grundyValue_ne_moveLeft` 📖	—	—	—	—	`grundyValue_eq_sInf_moveLeft` `csInf_mem` `Nimber.instWellFoundedLT` `nonempty_of_not_bddAbove` `Nimber.not_bddAbove_compl_of_small` `small_range` `UnivLE.small` `UnivLE.self` `Set.mem_range` `Set.mem_compl_iff`
`grundyValue_ne_moveRight` 📖	—	—	—	—	`moveLeft_neg` `Equiv.symm_apply_apply` `grundyValue_neg` `Impartial.moveRight_impartial` `grundyValue_ne_moveLeft`
`grundyValue_neg` 📖	mathematical	—	`grundyValue` `SetTheory.PGame` `instNeg`	—	`grundyValue_eq_iff_equiv_nim` `Impartial.impartial_neg` `neg_equiv_iff` `neg_nim`
`grundyValue_nim_add_nim` 📖	mathematical	—	`grundyValue` `SetTheory.PGame` `instAdd` `nim` `Nimber` `Nimber.instAdd` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nimber.instLinearOrder` `instFunLikeOrderIso` `Ordinal.toNimber`	—	—
`grundyValue_star` 📖	mathematical	—	`grundyValue` `star` `Nimber` `instOneNimber`	—	`grundyValue_eq_iff_equiv_nim` `Impartial.impartial_star` `Equiv.symm` `nim_one_equiv`
`grundyValue_zero` 📖	mathematical	—	`grundyValue` `SetTheory.PGame` `instZero` `Nimber` `instZeroNimber`	—	`grundyValue_eq_iff_equiv_nim` `Impartial.impartial_zero` `Equiv.symm` `nim_zero_equiv`
`impartial_nim` 📖	mathematical	—	`Impartial` `nim`	—	`Ordinal.induction` `impartial_def` `neg_nim` `equiv_rfl` `moveLeft_nim` `isWellOrder_lt` `wellFoundedLT_toType` `Ordinal.typein_lt_self` `moveRight_nim`
`isEmpty_nim_zero_leftMoves` 📖	mathematical	—	`IsEmpty` `LeftMoves` `nim` `Ordinal` `Ordinal.zero`	—	`nim.eq_1` `Ordinal.isEmpty_toType_zero`
`isEmpty_nim_zero_rightMoves` 📖	mathematical	—	`IsEmpty` `RightMoves` `nim` `Ordinal` `Ordinal.zero`	—	`nim.eq_1` `Ordinal.isEmpty_toType_zero`
`le_grundyValue_of_Iio_subset_moveLeft` 📖	mathematical	`Set` `Nimber` `Set.instHasSubset` `Set.Iio` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Nimber.instConditionallyCompleteLinearOrderBot` `Set.range` `LeftMoves` `SetTheory.PGame` `grundyValue` `moveLeft`	`Preorder.toLE`	—	`grundyValue_ne_moveLeft`
`le_grundyValue_of_Iio_subset_moveRight` 📖	mathematical	`Set` `Nimber` `Set.instHasSubset` `Set.Iio` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Nimber.instConditionallyCompleteLinearOrderBot` `Set.range` `RightMoves` `SetTheory.PGame` `grundyValue` `moveRight`	`Preorder.toLE`	—	`grundyValue_ne_moveRight`
`leftMoves_nim` 📖	mathematical	—	`LeftMoves` `nim` `Ordinal.ToType`	—	`nim.eq_1`
`moveLeft_nim` 📖	mathematical	—	`moveLeft` `nim` `Ordinal` `Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `DFunLike.coe` `Equiv` `LeftMoves` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toLeftMovesNim`	—	`congr_heq` `moveLeft_nim_heq`
`moveLeft_nim_heq` 📖	mathematical	—	`moveLeft` `nim` `Ordinal` `Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.ToType.toOrd`	—	`nim.eq_1`
`moveLeft_toLeftMovesNim` 📖	mathematical	—	`moveLeft` `nim` `DFunLike.coe` `Equiv` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `LeftMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLeftMovesNim` `Set` `Set.instMembership`	—	`moveLeft_nim` `Equiv.symm_apply_apply`
`moveRight_nim` 📖	mathematical	—	`moveRight` `nim` `Ordinal` `Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `DFunLike.coe` `Equiv` `RightMoves` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toRightMovesNim`	—	`congr_heq` `moveRight_nim_heq`
`moveRight_nim_heq` 📖	mathematical	—	`moveRight` `nim` `Ordinal` `Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.ToType.toOrd`	—	`nim.eq_1`
`moveRight_toRightMovesNim` 📖	mathematical	—	`moveRight` `nim` `DFunLike.coe` `Equiv` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `RightMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `toRightMovesNim` `Set` `Set.instMembership`	—	`moveRight_nim` `Equiv.symm_apply_apply`
`neg_nim` 📖	mathematical	—	`SetTheory.PGame` `instNeg` `nim`	—	`Ordinal.induction` `nim.eq_1` `Ordinal.typein_lt_self`
`nim_add_equiv_zero_iff` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instAdd` `nim` `instZero`	—	`not_imp_not` `Impartial.not_equiv_zero_iff` `Impartial.impartial_add` `impartial_nim` `Impartial.fuzzy_zero_iff_gf` `zero_lf_le` `add_moveLeft_inr` `moveLeft_nim` `Equiv.symm_apply_apply` `Impartial.add_self` `fuzzy_congr_left` `add_comm_equiv` `Ne.lt_or_gt`
`nim_add_fuzzy_zero_iff` 📖	mathematical	—	`Fuzzy` `SetTheory.PGame` `instAdd` `nim` `instZero`	—	`iff_not_comm` `Impartial.not_fuzzy_zero_iff` `Impartial.impartial_add` `impartial_nim` `nim_add_equiv_zero_iff`
`nim_add_nim_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instAdd` `nim` `DFunLike.coe` `OrderIso` `Nimber` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nimber.instLinearOrder` `Ordinal.partialOrder` `instFunLikeOrderIso` `Nimber.toOrdinal` `Nimber.instAdd` `Ordinal.toNimber`	—	`grundyValue_eq_iff_equiv_nim` `Impartial.impartial_add` `impartial_nim` `grundyValue_nim_add_nim`
`nim_birthday` 📖	mathematical	—	`birthday` `nim`	—	`Ordinal.induction` `nim.eq_1` `birthday_def` `max_eq_right` `le_rfl` `isWellOrder_lt` `wellFoundedLT_toType` `Ordinal.typein_lt_self` `Ordinal.lsub_typein`
`nim_equiv_iff_eq` 📖	mathematical	—	`SetTheory.PGame` `setoid` `nim`	—	`Impartial.equiv_iff_add_equiv_zero` `impartial_nim` `nim_add_equiv_zero_iff`
`nim_fuzzy_zero_of_ne_zero` 📖	mathematical	—	`Fuzzy` `nim` `SetTheory.PGame` `instZero`	—	`Impartial.fuzzy_zero_iff_lf` `impartial_nim` `lf_zero_le` `pos_iff_ne_zero` `Ordinal.canonicallyOrderedAdd` `moveRight_nim` `Equiv.symm_apply_apply` `isEmpty_nim_zero_leftMoves`
`nim_grundyValue` 📖	mathematical	—	`grundyValue` `nim` `DFunLike.coe` `OrderIso` `Ordinal` `Nimber` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nimber.instLinearOrder` `instFunLikeOrderIso` `Ordinal.toNimber`	—	`grundyValue_eq_iff_equiv_nim` `impartial_nim` `equiv_rfl`
`nim_one_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `nim` `Ordinal` `Ordinal.one` `star`	—	`Relabelling.equiv`
`nim_one_moveLeft` 📖	mathematical	—	`moveLeft` `nim` `Ordinal` `Ordinal.one` `Ordinal.zero`	—	`moveLeft_nim` `Set.mem_Iio` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne` `toLeftMovesNim_one_symm`
`nim_one_moveRight` 📖	mathematical	—	`moveRight` `nim` `Ordinal` `Ordinal.one` `Ordinal.zero`	—	`moveRight_nim` `Set.mem_Iio` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne` `toRightMovesNim_one_symm`
`nim_zero_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `nim` `Ordinal` `Ordinal.zero` `instZero`	—	`Equiv.isEmpty` `isEmpty_nim_zero_leftMoves` `isEmpty_nim_zero_rightMoves`
`rightMoves_nim` 📖	mathematical	—	`RightMoves` `nim` `Ordinal.ToType`	—	`nim.eq_1`
`toLeftMovesNim_one_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LeftMoves` `nim` `Ordinal` `Ordinal.one` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toLeftMovesNim` `Set` `Set.instMembership` `Ordinal.zero` `Preorder.toLT` `Set.mem_Iio` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne`	—	`Set.mem_Iio` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne` `Unique.instSubsingleton`
`toLeftMovesNim_symm_lt` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Set` `Set.instMembership` `Set.Iio` `DFunLike.coe` `Equiv` `LeftMoves` `nim` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toLeftMovesNim`	—	`Subtype.prop`
`toRightMovesNim_one_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RightMoves` `nim` `Ordinal` `Ordinal.one` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toRightMovesNim` `Set` `Set.instMembership` `Ordinal.zero` `Preorder.toLT` `Set.mem_Iio` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne`	—	`Set.mem_Iio` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne` `Unique.instSubsingleton`
`toRightMovesNim_symm_lt` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Set` `Set.instMembership` `Set.Iio` `DFunLike.coe` `Equiv` `RightMoves` `nim` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `toRightMovesNim`	—	`Subtype.prop`

---

← Back to Index