Commit 2023-06-29 04:23 a0da6e77

View on Github →

feat: port SetTheory.Surreal.Dyadic (#5552)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/SetTheory/Game/PGame.lean

Created Mathlib/SetTheory/Surreal/Dyadic.lean

added theorem PGame.add_powHalf_succ_self_eq_powHalf

added theorem PGame.birthday_half

added theorem PGame.half_add_half_equiv_one

added theorem PGame.numeric_powHalf

added def PGame.powHalf

added theorem PGame.powHalf_le_one

added theorem PGame.powHalf_leftMoves

added theorem PGame.powHalf_moveLeft

added theorem PGame.powHalf_pos

added theorem PGame.powHalf_succ_le_powHalf

added theorem PGame.powHalf_succ_lt_one

added theorem PGame.powHalf_succ_lt_powHalf

added theorem PGame.powHalf_succ_moveRight

added theorem PGame.powHalf_succ_rightMoves

added theorem PGame.powHalf_zero

added theorem PGame.powHalf_zero_rightMoves

added theorem PGame.zero_le_powHalf

added theorem Surreal.double_powHalf_succ_eq_powHalf

added def Surreal.dyadic

added def Surreal.dyadicMap

added theorem Surreal.dyadicMap_apply

added theorem Surreal.dyadicMap_apply_pow'

added theorem Surreal.dyadicMap_apply_pow

added theorem Surreal.dyadic_aux

added theorem Surreal.nsmul_pow_two_powHalf'

added theorem Surreal.nsmul_pow_two_powHalf

added def Surreal.powHalf

added theorem Surreal.powHalf_zero

added theorem Surreal.zsmul_pow_two_powHalf