Documentation Verification Report

Dyadic

📁 Source: Mathlib/SetTheory/Surreal/Dyadic.lean

Statistics

Metric	Count
Definitions `powHalf`, `uniquePowHalfLeftMoves`, `uniquePowHalfSuccRightMoves`, `dyadic`, `dyadicMap`, `powHalf`	6
Theorems `add_powHalf_succ_self_eq_powHalf`, `birthday_half`, `half_add_half_equiv_one`, `isEmpty_powHalf_zero_rightMoves`, `numeric_powHalf`, `powHalf_le_one`, `powHalf_leftMoves`, `powHalf_moveLeft`, `powHalf_pos`, `powHalf_succ_le_powHalf`, `powHalf_succ_lt_one`, `powHalf_succ_lt_powHalf`, `powHalf_succ_moveRight`, `powHalf_succ_rightMoves`, `powHalf_zero`, `powHalf_zero_rightMoves`, `zero_le_powHalf`, `double_powHalf_succ_eq_powHalf`, `dyadicMap_apply`, `dyadicMap_apply_pow`, `dyadicMap_apply_pow'`, `dyadic_aux`, `nsmul_pow_two_powHalf`, `nsmul_pow_two_powHalf'`, `powHalf_zero`, `zsmul_pow_two_powHalf`	26
Total	32

SetTheory.PGame

Definitions

Name	Category	Theorems
`powHalf` 📖	CompOp	17 math math: `powHalf_succ_lt_one`, `isEmpty_powHalf_zero_rightMoves`, `powHalf_succ_lt_powHalf`, `powHalf_leftMoves`, `powHalf_le_one`, `powHalf_succ_le_powHalf`, `birthday_half`, `numeric_powHalf`, `powHalf_moveLeft`, `powHalf_pos`, `add_powHalf_succ_self_eq_powHalf`, `zero_le_powHalf`, `powHalf_succ_rightMoves`, `half_add_half_equiv_one`, `powHalf_zero`, `powHalf_succ_moveRight`, `powHalf_zero_rightMoves`
`uniquePowHalfLeftMoves` 📖	CompOp	—
`uniquePowHalfSuccRightMoves` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_powHalf_succ_self_eq_powHalf` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instAdd` `powHalf`	—	`Nat.strong_induction_on` `le_iff_forall_lf` `lf_of_lt` `zero_add_equiv` `powHalf_succ_lt_powHalf` `add_zero_equiv` `lf_of_moveRight_le` `le_imp_le_of_le_of_le` `add_le_add_right` `addLeftMono` `powHalf_succ_le_powHalf` `le_refl` `powHalf_moveLeft` `Equiv.symm` `add_le_add_left` `addRightMono` `zero_le_powHalf` `add_lt_add_right` `addLeftStrictMono` `powHalf_pos` `add_lt_add_left` `addRightStrictMono`
`birthday_half` 📖	mathematical	—	`birthday` `powHalf` `Ordinal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `birthday_def` `powHalf_moveLeft` `birthday_zero` `Ordinal.lsub_unique` `Ordinal.succ_zero` `birthday_one` `Ordinal.succ_one` `sup_of_le_right` `Ordinal.instAddLeftMono` `Ordinal.instZeroLEOneClass` `Ordinal.instCharZero`
`half_add_half_equiv_one` 📖	mathematical	—	`SetTheory.PGame` `setoid` `instAdd` `powHalf` `instOnePGame`	—	`add_powHalf_succ_self_eq_powHalf`
`isEmpty_powHalf_zero_rightMoves` 📖	mathematical	—	`IsEmpty` `RightMoves` `powHalf`	—	`PEmpty.instIsEmpty`
`numeric_powHalf` 📖	mathematical	—	`Numeric` `powHalf`	—	`numeric_one` `powHalf_moveLeft` `Numeric.moveLeft_lt` `numeric_zero`
`powHalf_le_one` 📖	mathematical	—	`SetTheory.PGame` `le` `powHalf` `instOnePGame`	—	`le_rfl` `LE.le.trans` `powHalf_succ_le_powHalf`
`powHalf_leftMoves` 📖	mathematical	—	`LeftMoves` `powHalf`	—	—
`powHalf_moveLeft` 📖	mathematical	—	`moveLeft` `powHalf` `SetTheory.PGame` `instZero`	—	—
`powHalf_pos` 📖	mathematical	—	`SetTheory.PGame` `Preorder.toLT` `instPreorder` `instZero` `powHalf`	—	`lf_iff_lt` `numeric_zero` `numeric_powHalf` `zero_lf_le` `powHalf_moveLeft`
`powHalf_succ_le_powHalf` 📖	mathematical	—	`SetTheory.PGame` `le` `powHalf`	—	`LT.lt.le` `powHalf_succ_lt_powHalf`
`powHalf_succ_lt_one` 📖	mathematical	—	`SetTheory.PGame` `Preorder.toLT` `instPreorder` `powHalf` `instOnePGame`	—	`LT.lt.trans_le` `powHalf_succ_lt_powHalf` `powHalf_le_one`
`powHalf_succ_lt_powHalf` 📖	mathematical	—	`SetTheory.PGame` `Preorder.toLT` `instPreorder` `powHalf`	—	`Numeric.lt_moveRight` `numeric_powHalf`
`powHalf_succ_moveRight` 📖	mathematical	—	`moveRight` `powHalf`	—	—
`powHalf_succ_rightMoves` 📖	mathematical	—	`RightMoves` `powHalf`	—	—
`powHalf_zero` 📖	mathematical	—	`powHalf` `SetTheory.PGame` `instOnePGame`	—	—
`powHalf_zero_rightMoves` 📖	mathematical	—	`RightMoves` `powHalf`	—	—
`zero_le_powHalf` 📖	mathematical	—	`SetTheory.PGame` `le` `instZero` `powHalf`	—	`LT.lt.le` `powHalf_pos`

Surreal

Definitions

Name	Category	Theorems
`dyadic` 📖	CompOp	—
`dyadicMap` 📖	CompOp	2 math math: `dyadicMap_apply`, `dyadicMap_apply_pow`
`powHalf` 📖	CompOp	9 math math: `nsmul_pow_two_powHalf`, `zsmul_pow_two_powHalf`, `dyadicMap_apply_pow'`, `powHalf_zero`, `dyadicMap_apply`, `dyadic_aux`, `double_powHalf_succ_eq_powHalf`, `dyadicMap_apply_pow`, `nsmul_pow_two_powHalf'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`double_powHalf_succ_eq_powHalf` 📖	mathematical	—	`Surreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `powHalf`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `SetTheory.PGame.numeric_powHalf` `SetTheory.PGame.Numeric.add` `SetTheory.PGame.add_powHalf_succ_self_eq_powHalf`
`dyadicMap_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Localization.Away` `Int.instCommMonoid` `Surreal` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `OreLocalization.instAddMonoid` `CommMonoid.toMonoid` `Submonoid.powers` `OreLocalization.oreSetComm` `AddCommMonoid.toAddMonoid` `Int.instAddCommMonoid` `Module.toDistribMulAction` `Int.instSemiring` `AddCommGroup.toIntModule` `Int.instAddCommGroup` `AddMonoidWithOne.toAddMonoid` `instAddMonoidWithOne` `AddMonoidHom.instFunLike` `dyadicMap` `IsLocalization.mk'` `Int.instCommSemiring` `Int.instMonoid` `Localization` `OreLocalization.instCommSemiring` `OreLocalization.instAlgebra` `Algebra.id` `Localization.isLocalization` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `powHalf` `Submonoid.log`	—	`Localization.isLocalization` `Localization.mk_eq_mk'`
`dyadicMap_apply_pow` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Localization.Away` `Int.instCommMonoid` `Surreal` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `OreLocalization.instAddMonoid` `CommMonoid.toMonoid` `Submonoid.powers` `OreLocalization.oreSetComm` `AddCommMonoid.toAddMonoid` `Int.instAddCommMonoid` `Module.toDistribMulAction` `Int.instSemiring` `AddCommGroup.toIntModule` `Int.instAddCommGroup` `AddMonoidWithOne.toAddMonoid` `instAddMonoidWithOne` `AddMonoidHom.instFunLike` `dyadicMap` `IsLocalization.mk'` `Int.instCommSemiring` `Int.instMonoid` `Localization` `OreLocalization.instCommSemiring` `OreLocalization.instAlgebra` `Algebra.id` `Localization.isLocalization` `Submonoid.pow` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `powHalf`	—	`Localization.isLocalization` `dyadicMap_apply` `Submonoid.log_pow_int_eq_self` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `zsmul_eq_mul`
`dyadicMap_apply_pow'` 📖	mathematical	—	`Surreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `powHalf` `Submonoid.log` `Int.instMonoid` `Submonoid.pow`	—	`Submonoid.log_pow_int_eq_self` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`dyadic_aux` 📖	mathematical	`Monoid.toNatPow` `Int.instMonoid`	`Surreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `powHalf`	—	`le_iff_exists_add` `Nat.instCanonicallyOrderedAdd` `mul_eq_mul_right_iff` `IsCancelMulZero.toIsRightCancelMulZero` `Int.instIsCancelMulZero` `mul_assoc` `pow_add` `add_comm` `Int.cast_mul` `Int.cast_pow` `Nat.instAtLeastTwoHAddOfNat` `Int.cast_ofNat` `zsmul_pow_two_powHalf` `Nat.succ_pos'` `Nat.cast_zero` `Int.instCharZero` `le_of_not_ge`
`nsmul_pow_two_powHalf` 📖	mathematical	—	`Surreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `powHalf` `instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_zero` `mul_one` `double_powHalf_succ_eq_powHalf` `mul_assoc` `pow_succ'` `mul_comm`
`nsmul_pow_two_powHalf'` 📖	mathematical	—	`Surreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `powHalf`	—	`Nat.instAtLeastTwoHAddOfNat` `add_zero` `nsmul_pow_two_powHalf` `zsmul_eq_zsmul_iff'` `instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `two_ne_zero` `zsmul_eq_mul` `Int.cast_ofNat` `mul_assoc` `mul_comm` `double_powHalf_succ_eq_powHalf`
`powHalf_zero` 📖	mathematical	—	`powHalf` `Surreal` `instOne`	—	—
`zsmul_pow_two_powHalf` 📖	mathematical	—	`Surreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `powHalf`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_assoc` `nsmul_pow_two_powHalf'`

---

← Back to Index