Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-09 16:05 983fdd6b

View on Github →

chore(set_theory/ordinal/arithmetic): review cast API (#14757) This PR does the following:

  • swap the direction of nat_cast_succ to match nat.cast_succ.
  • make various arguments explicit.
  • remove lift_type_fin, as it's a trivial consequence of type_fin and lift_nat_cast.
  • tag various theorems as norm_cast.
  • golf or otherwise cleanup various proofs.

Estimated changes

modified theorem ordinal.lift_nat_cast
deleted theorem ordinal.lift_type_fin
modified theorem ordinal.nat_cast_div
modified theorem ordinal.nat_cast_eq_zero
modified theorem ordinal.nat_cast_inj
modified theorem ordinal.nat_cast_le
modified theorem ordinal.nat_cast_lt
modified theorem ordinal.nat_cast_mod
modified theorem ordinal.nat_cast_mul
modified theorem ordinal.nat_cast_opow
modified theorem ordinal.nat_cast_pos
modified theorem ordinal.nat_cast_sub
modified theorem ordinal.nat_cast_succ