Basic

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

Statistics

Metric	Count
Definitions `Game`, `Fuzzy`, `LF`, `instAdd`, `instAddCommGroupWithOneGame`, `instInhabited`, `instNeg`, `instPartialOrderGame`, `instZero`, `InvTy`, `instInhabited`, `instDiv`, `instInv`, `instMul`, `inv'`, `inv'One`, `inv'Zero`, `invOne`, `invVal`, `mulCommRelabelling`, `mulNegRelabelling`, `mulOneRelabelling`, `mulOption`, `mulZeroRelabelling`, `negMulRelabelling`, `oneMulRelabelling`, `toLeftMovesMul`, `toRightMovesMul`, `uniqueInvTy`, `zeroMulRelabelling`	30
Theorems `addLeftMono`, `addLeftStrictMono`, `addRightMono`, `addRightStrictMono`, `add_lf_add_left`, `add_lf_add_right`, `bddAbove_of_small`, `bddAbove_range_of_small`, `bddBelow_of_small`, `bddBelow_range_of_small`, `instTrichotomousLF`, `isOrderedAddMonoid`, `not_le`, `not_lf`, `zero_def`, `equiv_iff_game_eq`, `fuzzy_iff_game_fuzzy`, `game_eq`, `instIsEmptyInvTyTrue`, `inv'_one`, `inv'_one_equiv`, `inv'_zero_equiv`, `invVal_isEmpty`, `inv_eq_of_equiv_zero`, `inv_eq_of_lf_zero`, `inv_eq_of_pos`, `inv_one`, `inv_one_equiv`, `inv_zero`, `isEmpty_leftMoves_mul`, `isEmpty_rightMoves_mul`, `le_iff_game_le`, `leftMoves_mul`, `leftMoves_mul_cases`, `leftMoves_mul_iff`, `left_distrib_equiv`, `lf_iff_game_lf`, `lt_iff_game_lt`, `mk_mul_moveLeft_inl`, `mk_mul_moveLeft_inr`, `mk_mul_moveRight_inl`, `mk_mul_moveRight_inr`, `mulOption_neg_neg`, `mulOption_symm`, `mul_assoc_equiv`, `mul_comm`, `mul_comm_equiv`, `mul_moveLeft_inl`, `mul_moveLeft_inr`, `mul_moveRight_inl`, `mul_moveRight_inr`, `mul_neg`, `mul_one`, `mul_one_equiv`, `mul_zero`, `mul_zero_equiv`, `neg_mk_mul_moveLeft_inl`, `neg_mk_mul_moveLeft_inr`, `neg_mk_mul_moveRight_inl`, `neg_mk_mul_moveRight_inr`, `neg_mul`, `one_mul`, `one_mul_equiv`, `quot_add`, `quot_eq_of_mk'_quot_eq`, `quot_left_distrib`, `quot_left_distrib_sub`, `quot_mul_assoc`, `quot_mul_comm`, `quot_mul_neg`, `quot_mul_one`, `quot_mul_zero`, `quot_natCast`, `quot_neg`, `quot_neg_mul`, `quot_neg_mul_neg`, `quot_one`, `quot_one_mul`, `quot_right_distrib`, `quot_right_distrib_sub`, `quot_sub`, `quot_zero`, `quot_zero_mul`, `rightMoves_mul`, `rightMoves_mul_cases`, `rightMoves_mul_iff`, `right_distrib_equiv`, `zero_lf_inv'`, `zero_mul`, `zero_mul_equiv`	90
Total	120

SetTheory

Definitions

Name	Category	Theorems
`Game` 📖	CompOp	41 math math: `Game.birthday_add_le`, `Game.birthday_neg`, `Game.addLeftMono`, `Game.birthday_sub_le`, `Game.birthday_natCast`, `Ordinal.toGame_lt_iff`, `Game.not_le`, `Ordinal.toGame_one`, `PGame.quot_natCast`, `Game.zero_def`, `Game.birthday_zero`, `Game.birthday_one`, `Game.birthday_ordinalToGame`, `Game.le_birthday`, `Game.instTrichotomousLF`, `Game.birthday_eq_zero`, `Game.bddBelow_of_small`, `Ordinal.mk_toPGame`, `Game.isOrderedAddMonoid`, `Ordinal.toGame_zero`, `Game.addRightStrictMono`, `Game.addRightMono`, `Ordinal.toGame_nmul`, `Surreal.nat_toGame`, `Ordinal.toGame_lf_iff`, `Game.bddAbove_range_of_small`, `Game.small_setOf_birthday_lt`, `Ordinal.toGame_inj`, `Game.neg_birthday_le`, `Game.add_lf_add_left`, `Surreal.zero_toGame`, `Game.bddBelow_range_of_small`, `Game.bddAbove_of_small`, `Ordinal.toGame_injective`, `Game.add_lf_add_right`, `Surreal.one_toGame`, `Ordinal.toGame_nadd`, `Game.addLeftStrictMono`, `Ordinal.toGame_natCast`, `Game.not_lf`, `Ordinal.toGame_le_iff`

SetTheory.Game

Definitions

Name	Category	Theorems
`Fuzzy` 📖	MathDef	1 math math: `SetTheory.PGame.fuzzy_iff_game_fuzzy`
`LF` 📖	MathDef	5 math math: `not_le`, `instTrichotomousLF`, `Ordinal.toGame_lf_iff`, `SetTheory.PGame.lf_iff_game_lf`, `not_lf`
`instAdd` 📖	CompOp	12 math math: `birthday_add_le`, `addLeftMono`, `SetTheory.PGame.Impartial.mk'_add_self`, `SetTheory.PGame.quot_left_distrib`, `addRightStrictMono`, `addRightMono`, `add_lf_add_left`, `SetTheory.PGame.quot_right_distrib`, `add_lf_add_right`, `SetTheory.PGame.quot_add`, `Ordinal.toGame_nadd`, `addLeftStrictMono`
`instAddCommGroupWithOneGame` 📖	CompOp	14 math math: `birthday_sub_le`, `SetTheory.PGame.quot_one`, `birthday_natCast`, `SetTheory.PGame.quot_right_distrib_sub`, `Ordinal.toGame_one`, `SetTheory.PGame.quot_natCast`, `SetTheory.PGame.quot_left_distrib_sub`, `birthday_one`, `isOrderedAddMonoid`, `Surreal.nat_toGame`, `Surreal.zero_toGame`, `SetTheory.PGame.quot_sub`, `Surreal.one_toGame`, `Ordinal.toGame_natCast`
`instInhabited` 📖	CompOp	—
`instNeg` 📖	CompOp	10 math math: `birthday_neg`, `SetTheory.PGame.quot_neg_mul`, `SetTheory.PGame.quot_mul_neg`, `SetTheory.PGame.rightMoves_mul_iff`, `Surreal.Multiplication.mulOption_lt`, `SetTheory.PGame.Impartial.mk'_neg_equiv_self`, `Surreal.Multiplication.mulOption_lt_iff_P1`, `neg_birthday_le`, `Surreal.Multiplication.mulOption_lt_of_lt`, `SetTheory.PGame.quot_neg`
`instPartialOrderGame` 📖	CompOp	35 math math: `addLeftMono`, `Ordinal.toGame_lt_iff`, `Surreal.Multiplication.mulOption_lt_mul_iff_P3`, `not_le`, `Ordinal.toGame_one`, `SetTheory.PGame.lt_iff_game_lt`, `Surreal.Multiplication.mulOption_lt_mul_of_equiv`, `birthday_ordinalToGame`, `le_birthday`, `Surreal.Multiplication.mulOption_lt`, `bddBelow_of_small`, `Ordinal.mk_toPGame`, `isOrderedAddMonoid`, `Ordinal.toGame_zero`, `addRightStrictMono`, `Surreal.Multiplication.mulOption_lt_iff_P1`, `addRightMono`, `Ordinal.toGame_nmul`, `Surreal.nat_toGame`, `Ordinal.toGame_lf_iff`, `bddAbove_range_of_small`, `SetTheory.PGame.le_iff_game_le`, `Ordinal.toGame_inj`, `neg_birthday_le`, `Surreal.Multiplication.mulOption_lt_of_lt`, `Surreal.zero_toGame`, `bddBelow_range_of_small`, `bddAbove_of_small`, `Ordinal.toGame_injective`, `Surreal.one_toGame`, `Ordinal.toGame_nadd`, `addLeftStrictMono`, `Ordinal.toGame_natCast`, `not_lf`, `Ordinal.toGame_le_iff`
`instZero` 📖	CompOp	9 math math: `SetTheory.PGame.Impartial.mk'_add_self`, `zero_def`, `birthday_zero`, `birthday_eq_zero`, `Ordinal.toGame_zero`, `SetTheory.PGame.quot_mul_zero`, `Surreal.zero_toGame`, `SetTheory.PGame.quot_zero_mul`, `SetTheory.PGame.quot_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `SetTheory.Game` `instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame`	—	`add_le_add_right` `SetTheory.PGame.addLeftMono`
`addLeftStrictMono` 📖	mathematical	—	`AddLeftStrictMono` `SetTheory.Game` `instAdd` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderGame`	—	`add_lt_add_right` `SetTheory.PGame.addLeftStrictMono`
`addRightMono` 📖	mathematical	—	`AddRightMono` `SetTheory.Game` `instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame`	—	`add_le_add_left` `SetTheory.PGame.addRightMono`
`addRightStrictMono` 📖	mathematical	—	`AddRightStrictMono` `SetTheory.Game` `instAdd` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderGame`	—	`add_lt_add_left` `SetTheory.PGame.addRightStrictMono`
`add_lf_add_left` 📖	mathematical	`LF`	`SetTheory.Game` `instAdd`	—	`SetTheory.PGame.add_lf_add_left`
`add_lf_add_right` 📖	mathematical	`LF`	`SetTheory.Game` `instAdd`	—	`SetTheory.PGame.add_lf_add_right`
`bddAbove_of_small` 📖	mathematical	—	`BddAbove` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame`	—	`Subtype.range_coe_subtype` `bddAbove_range_of_small`
`bddAbove_range_of_small` 📖	mathematical	—	`BddAbove` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame` `Set.range`	—	`SetTheory.PGame.bddAbove_range_of_small` `Set.forall_mem_range` `Quotient.out_eq` `Set.mem_range_self`
`bddBelow_of_small` 📖	mathematical	—	`BddBelow` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame`	—	`Subtype.range_coe_subtype` `bddBelow_range_of_small`
`bddBelow_range_of_small` 📖	mathematical	—	`BddBelow` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame` `Set.range`	—	`SetTheory.PGame.bddBelow_range_of_small` `Set.forall_mem_range` `Quotient.out_eq` `Set.mem_range_self`
`instTrichotomousLF` 📖	mathematical	—	`SetTheory.Game` `LF`	—	`Quotient.eq` `SetTheory.PGame.lf_or_equiv_or_gf`
`isOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `SetTheory.Game` `AddCommMonoidWithOne.toAddCommMonoid` `AddCommGroupWithOne.toAddCommMonoidWithOne` `instAddCommGroupWithOneGame` `instPartialOrderGame`	—	`add_le_add_left` `addRightMono`
`not_le` 📖	mathematical	—	`SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame` `LF`	—	`SetTheory.PGame.not_le`
`not_lf` 📖	mathematical	—	`LF` `SetTheory.Game` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderGame`	—	`SetTheory.PGame.not_lf`
`zero_def` 📖	mathematical	—	`SetTheory.Game` `instZero` `SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instZero`	—	—

SetTheory.PGame

Definitions

Name	Category	Theorems
`InvTy` 📖	CompData	1 math math: `instIsEmptyInvTyTrue`
`instDiv` 📖	CompOp	—
`instInv` 📖	CompOp	6 math math: `inv_eq_of_pos`, `inv_one_equiv`, `inv_eq_of_lf_zero`, `inv_zero`, `inv_eq_of_equiv_zero`, `inv_one`
`instMul` 📖	CompOp	61 math math: `quot_neg_mul`, `right_distrib_equiv`, `mk_mul_moveRight_inl`, `one_mul_equiv`, `Surreal.Multiplication.numeric_mul_option`, `Surreal.Multiplication.mulOption_lt_mul_iff_P3`, `isEmpty_leftMoves_mul`, `quot_right_distrib_sub`, `neg_mk_mul_moveRight_inl`, `quot_mul_neg`, `mul_moveRight_inl`, `Ordinal.toPGame_nmul`, `rightMoves_mul_iff`, `mul_moveRight_inr`, `quot_mul_one`, `mul_moveLeft_inl`, `Surreal.Multiplication.numeric_of_ih`, `neg_mk_mul_moveLeft_inr`, `quot_left_distrib_sub`, `Surreal.Multiplication.mulOption_lt_mul_of_equiv`, `Numeric.mul`, `mul_one_equiv`, `mul_moveLeft_inr`, `Surreal.Multiplication.numeric_option_mul_option`, `mul_zero_equiv`, `quot_left_distrib`, `left_distrib_equiv`, `zero_mul`, `mul_assoc_equiv`, `quot_one_mul`, `leftMoves_mul_iff`, `Surreal.Multiplication.mul_right_le_of_equiv`, `Equiv.mul_congr_right`, `mul_comm_equiv`, `quot_mul_comm`, `rightMoves_mul`, `Ordinal.toGame_nmul`, `quot_mul_zero`, `Surreal.Multiplication.numeric_option_mul`, `Surreal.Multiplication.P1_of_ih`, `zero_mul_equiv`, `quot_mul_assoc`, `leftMoves_mul`, `one_mul`, `mk_mul_moveLeft_inl`, `Equiv.mul_congr`, `Numeric.mul_pos`, `mk_mul_moveRight_inr`, `quot_right_distrib`, `isEmpty_rightMoves_mul`, `quot_zero_mul`, `Equiv.mul_congr_left`, `neg_mk_mul_moveLeft_inl`, `mk_mul_moveLeft_inr`, `mul_one`, `mul_neg`, `neg_mk_mul_moveRight_inr`, `quot_neg_mul_neg`, `mul_comm`, `neg_mul`, `mul_zero`
`inv'` 📖	CompOp	6 math math: `inv_eq_of_pos`, `inv'_one_equiv`, `zero_lf_inv'`, `inv'_one`, `inv_eq_of_lf_zero`, `inv'_zero_equiv`
`inv'One` 📖	CompOp	—
`inv'Zero` 📖	CompOp	—
`invOne` 📖	CompOp	—
`invVal` 📖	CompOp	1 math math: `invVal_isEmpty`
`mulCommRelabelling` 📖	CompOp	—
`mulNegRelabelling` 📖	CompOp	—
`mulOneRelabelling` 📖	CompOp	—
`mulOption` 📖	CompOp	9 math math: `Surreal.Multiplication.mulOption_lt_mul_iff_P3`, `mulOption_neg_neg`, `rightMoves_mul_iff`, `Surreal.Multiplication.mulOption_lt_mul_of_equiv`, `Surreal.Multiplication.mulOption_lt`, `mulOption_symm`, `leftMoves_mul_iff`, `Surreal.Multiplication.mulOption_lt_iff_P1`, `Surreal.Multiplication.mulOption_lt_of_lt`
`mulZeroRelabelling` 📖	CompOp	—
`negMulRelabelling` 📖	CompOp	—
`oneMulRelabelling` 📖	CompOp	—
`toLeftMovesMul` 📖	CompOp	2 math math: `mul_moveLeft_inl`, `mul_moveLeft_inr`
`toRightMovesMul` 📖	CompOp	2 math math: `mul_moveRight_inl`, `mul_moveRight_inr`
`uniqueInvTy` 📖	CompOp	—
`zeroMulRelabelling` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_iff_game_eq` 📖	mathematical	—	`SetTheory.PGame` `setoid`	—	`Quotient.eq'`
`fuzzy_iff_game_fuzzy` 📖	mathematical	—	`Fuzzy` `SetTheory.Game.Fuzzy` `SetTheory.PGame` `setoid`	—	—
`game_eq` 📖	—	`SetTheory.PGame` `setoid`	—	—	`equiv_iff_game_eq`
`instIsEmptyInvTyTrue` 📖	mathematical	—	`IsEmpty` `InvTy`	—	—
`inv'_one` 📖	mathematical	—	`Identical` `inv'` `SetTheory.PGame` `instOnePGame`	—	`Identical.ext_iff` `invVal_isEmpty` `PEmpty.instIsEmpty` `instIsEmptyInvTyTrue` `Subtype.isEmpty_false`
`inv'_one_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `inv'` `instOnePGame`	—	`Identical.equiv` `inv'_one`
`inv'_zero_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `inv'` `instZero` `instOnePGame`	—	`Relabelling.equiv`
`invVal_isEmpty` 📖	mathematical	—	`invVal` `SetTheory.PGame` `instZero`	—	—
`inv_eq_of_equiv_zero` 📖	mathematical	`SetTheory.PGame` `setoid` `instZero`	`instInv`	—	—
`inv_eq_of_lf_zero` 📖	mathematical	`LF` `SetTheory.PGame` `instZero`	`instInv` `instNeg` `inv'`	—	`LF.not_equiv` `LF.not_gt`
`inv_eq_of_pos` 📖	mathematical	`SetTheory.PGame` `Preorder.toLT` `instPreorder` `instZero`	`instInv` `inv'`	—	`LF.not_equiv'` `LT.lt.lf`
`inv_one` 📖	mathematical	—	`Identical` `SetTheory.PGame` `instInv` `instOnePGame`	—	`inv_eq_of_pos` `zero_lt_one` `inv'_one`
`inv_one_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instInv` `instOnePGame`	—	`Identical.equiv` `inv_one`
`inv_zero` 📖	mathematical	—	`SetTheory.PGame` `instInv` `instZero`	—	`inv_eq_of_equiv_zero` `equiv_refl`
`isEmpty_leftMoves_mul` 📖	mathematical	—	`IsEmpty` `LeftMoves` `SetTheory.PGame` `instMul`	—	—
`isEmpty_rightMoves_mul` 📖	mathematical	—	`IsEmpty` `RightMoves` `SetTheory.PGame` `instMul`	—	—
`le_iff_game_le` 📖	mathematical	—	`SetTheory.PGame` `le` `setoid` `Preorder.toLE` `PartialOrder.toPreorder` `SetTheory.Game.instPartialOrderGame`	—	—
`leftMoves_mul` 📖	mathematical	—	`LeftMoves` `SetTheory.PGame` `instMul` `RightMoves`	—	—
`leftMoves_mul_cases` 📖	—	`DFunLike.coe` `Equiv` `LeftMoves` `RightMoves` `SetTheory.PGame` `instMul` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLeftMovesMul`	—	—	`Equiv.apply_symm_apply`
`leftMoves_mul_iff` 📖	mathematical	—	`SetTheory.PGame` `setoid` `moveLeft` `instMul` `mulOption` `instNeg`	—	`neg_def` `quot_neg_mul_neg`
`left_distrib_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instAdd`	—	`quot_left_distrib`
`lf_iff_game_lf` 📖	mathematical	—	`LF` `SetTheory.Game.LF` `SetTheory.PGame` `setoid`	—	—
`lt_iff_game_lt` 📖	mathematical	—	`SetTheory.PGame` `Preorder.toLT` `instPreorder` `setoid` `PartialOrder.toPreorder` `SetTheory.Game.instPartialOrderGame`	—	—
`mk_mul_moveLeft_inl` 📖	mathematical	—	`moveLeft` `SetTheory.PGame` `instMul` `instSub` `instAdd`	—	—
`mk_mul_moveLeft_inr` 📖	mathematical	—	`moveLeft` `SetTheory.PGame` `instMul` `instSub` `instAdd`	—	—
`mk_mul_moveRight_inl` 📖	mathematical	—	`moveRight` `SetTheory.PGame` `instMul` `instSub` `instAdd`	—	—
`mk_mul_moveRight_inr` 📖	mathematical	—	`moveRight` `SetTheory.PGame` `instMul` `instSub` `instAdd`	—	—
`mulOption_neg_neg` 📖	mathematical	—	`mulOption` `SetTheory.PGame` `instNeg` `DFunLike.coe` `Equiv` `RightMoves` `LeftMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLeftMovesNeg` `toRightMovesNeg`	—	`neg_neg` `moveLeft_neg` `Equiv.symm_apply_apply` `moveRight_neg`
`mulOption_symm` 📖	mathematical	—	`SetTheory.PGame` `setoid` `mulOption`	—	`add_comm` `quot_mul_comm`
`mul_assoc_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul`	—	`quot_mul_assoc`
`mul_comm` 📖	mathematical	—	`Identical` `SetTheory.PGame` `instMul`	—	—
`mul_comm_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul`	—	`quot_mul_comm`
`mul_moveLeft_inl` 📖	mathematical	—	`moveLeft` `SetTheory.PGame` `instMul` `DFunLike.coe` `Equiv` `LeftMoves` `RightMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLeftMovesMul` `instSub` `instAdd`	—	—
`mul_moveLeft_inr` 📖	mathematical	—	`moveLeft` `SetTheory.PGame` `instMul` `DFunLike.coe` `Equiv` `LeftMoves` `RightMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLeftMovesMul` `instSub` `instAdd` `moveRight`	—	—
`mul_moveRight_inl` 📖	mathematical	—	`moveRight` `SetTheory.PGame` `instMul` `DFunLike.coe` `Equiv` `LeftMoves` `RightMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `toRightMovesMul` `instSub` `instAdd` `moveLeft`	—	—
`mul_moveRight_inr` 📖	mathematical	—	`moveRight` `SetTheory.PGame` `instMul` `DFunLike.coe` `Equiv` `LeftMoves` `RightMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `toRightMovesMul` `instSub` `instAdd` `moveLeft`	—	—
`mul_neg` 📖	mathematical	—	`SetTheory.PGame` `instMul` `instNeg`	—	—
`mul_one` 📖	mathematical	—	`Identical` `SetTheory.PGame` `instMul` `instOnePGame`	—	`Identical.trans` `mul_comm` `one_mul`
`mul_one_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instOnePGame`	—	`quot_mul_one`
`mul_zero` 📖	mathematical	—	`Identical` `SetTheory.PGame` `instMul` `instZero`	—	`identical_zero` `isEmpty_leftMoves_mul` `instIsEmptySum` `Prod.isEmpty_right` `isEmpty_zero_leftMoves` `isEmpty_zero_rightMoves` `isEmpty_rightMoves_mul`
`mul_zero_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instZero`	—	`Identical.equiv` `mul_zero`
`neg_mk_mul_moveLeft_inl` 📖	mathematical	—	`moveLeft` `SetTheory.PGame` `instNeg` `instMul` `instSub` `instAdd`	—	—
`neg_mk_mul_moveLeft_inr` 📖	mathematical	—	`moveLeft` `SetTheory.PGame` `instNeg` `instMul` `instSub` `instAdd`	—	—
`neg_mk_mul_moveRight_inl` 📖	mathematical	—	`moveRight` `SetTheory.PGame` `instNeg` `instMul` `instSub` `instAdd`	—	—
`neg_mk_mul_moveRight_inr` 📖	mathematical	—	`moveRight` `SetTheory.PGame` `instNeg` `instMul` `instSub` `instAdd`	—	—
`neg_mul` 📖	mathematical	—	`Identical` `SetTheory.PGame` `instMul` `instNeg`	—	`Identical.trans` `mul_comm` `of_eq` `instReflIdentical` `mul_neg` `Identical.neg`
`one_mul` 📖	mathematical	—	`Identical` `SetTheory.PGame` `instMul` `instOnePGame`	—	`Identical.of_equiv` `Prod.isEmpty_left` `PEmpty.instIsEmpty` `Identical.trans` `Identical.sub` `Identical.add` `zero_mul` `zero_add` `sub_zero`
`one_mul_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instOnePGame`	—	`quot_one_mul`
`quot_add` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instAdd` `SetTheory.Game.instAdd`	—	—
`quot_eq_of_mk'_quot_eq` 📖	—	`SetTheory.PGame` `setoid` `moveLeft` `DFunLike.coe` `Equiv` `LeftMoves` `EquivLike.toFunLike` `Equiv.instEquivLike` `moveRight` `RightMoves`	—	—	`game_eq` `Equiv.of_equiv` `equiv_iff_game_eq`
`quot_left_distrib` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instAdd` `SetTheory.Game.instAdd`	—	—
`quot_left_distrib_sub` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame`	—	`quot_left_distrib` `quot_mul_neg`
`quot_mul_assoc` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul`	—	—
`quot_mul_comm` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul`	—	`game_eq` `Identical.equiv` `mul_comm`
`quot_mul_neg` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instNeg` `SetTheory.Game.instNeg`	—	`game_eq` `mul_neg`
`quot_mul_one` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instOnePGame`	—	`game_eq` `Identical.equiv` `mul_one`
`quot_mul_zero` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instZero` `SetTheory.Game.instZero`	—	`game_eq` `mul_zero_equiv`
`quot_natCast` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instNatCast` `SetTheory.Game` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame`	—	`nat_succ` `quot_add` `Nat.cast_add` `Nat.cast_one`
`quot_neg` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instNeg` `SetTheory.Game.instNeg`	—	—
`quot_neg_mul` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instNeg` `SetTheory.Game.instNeg`	—	`game_eq` `Identical.equiv` `neg_mul`
`quot_neg_mul_neg` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instNeg`	—	`mul_neg` `quot_neg_mul` `neg_neg`
`quot_one` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instOnePGame` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame`	—	—
`quot_one_mul` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instOnePGame`	—	`game_eq` `Identical.equiv` `one_mul`
`quot_right_distrib` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instAdd` `SetTheory.Game.instAdd`	—	`quot_mul_comm` `quot_left_distrib`
`quot_right_distrib_sub` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame`	—	`quot_right_distrib` `quot_neg_mul`
`quot_sub` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `SetTheory.Game.instAddCommGroupWithOneGame`	—	—
`quot_zero` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instZero` `SetTheory.Game.instZero`	—	—
`quot_zero_mul` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instZero` `SetTheory.Game.instZero`	—	`game_eq` `zero_mul_equiv`
`rightMoves_mul` 📖	mathematical	—	`RightMoves` `SetTheory.PGame` `instMul` `LeftMoves`	—	—
`rightMoves_mul_cases` 📖	—	`DFunLike.coe` `Equiv` `LeftMoves` `RightMoves` `SetTheory.PGame` `instMul` `EquivLike.toFunLike` `Equiv.instEquivLike` `toRightMovesMul`	—	—	`Equiv.apply_symm_apply`
`rightMoves_mul_iff` 📖	mathematical	—	`SetTheory.PGame` `setoid` `moveRight` `instMul` `SetTheory.Game.instNeg` `mulOption` `instNeg`	—	`neg_sub'` `neg_add` `neg_def` `quot_mul_neg` `neg_neg` `quot_neg_mul`
`right_distrib_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instAdd`	—	`quot_right_distrib`
`zero_lf_inv'` 📖	mathematical	—	`LF` `SetTheory.PGame` `instZero` `inv'`	—	—
`zero_mul` 📖	mathematical	—	`Identical` `SetTheory.PGame` `instMul` `instZero`	—	`identical_zero` `isEmpty_leftMoves_mul` `instIsEmptySum` `Prod.isEmpty_left` `isEmpty_zero_leftMoves` `isEmpty_zero_rightMoves` `isEmpty_rightMoves_mul`
`zero_mul_equiv` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instMul` `instZero`	—	`Identical.equiv` `zero_mul`

SetTheory.PGame.InvTy

Definitions

Name	Category	Theorems
`instInhabited` 📖	CompOp	—

---

← Back to Index