Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-13 08:58 716824d3

View on Github →

feat(set_theory/surreal/dyadic): tweak API + golf (#14649) This PR does the following changes:

  • Get rid of pgame.half, as it's def-eq to pow_half 1, which has strictly more API.
  • Fix the docstring on pow_half, which incorrectly stated pow_half 0 = 0.
  • Remove simp from some type equality lemmas.
  • Remove the redundant theorems pow_half_move_left' and pow_half_move_right'.
  • Add instances for left and right moves of pow_half.
  • Rename zero_lt_pow_half to pow_half_pos.
  • Prove pow_half_le_one and pow_half_succ_lt_one.
  • Make arguments explicit throughout.
  • Golf proofs throughout.

Estimated changes

deleted theorem pgame.birthday_half
deleted def pgame.half
deleted theorem pgame.half_left_moves
deleted theorem pgame.half_lt_one
deleted theorem pgame.half_move_left
deleted theorem pgame.half_move_right
deleted theorem pgame.half_right_moves
deleted theorem pgame.numeric_half
added theorem pgame.birthday_half
modified theorem pgame.numeric_pow_half
added theorem pgame.pow_half_le_one
modified theorem pgame.pow_half_left_moves
deleted theorem pgame.pow_half_move_left'
modified theorem pgame.pow_half_move_left
deleted theorem pgame.pow_half_move_right
added theorem pgame.pow_half_pos
added theorem pgame.pow_half_zero
modified theorem pgame.zero_le_pow_half
deleted theorem pgame.zero_lt_pow_half
deleted def surreal.half
modified def surreal.pow_half
deleted theorem surreal.pow_half_one