Commit 2024-04-18 21:51 5efe4b85

View on Github →

chore: use a variable in Data.Nat.Cast.Defs (#12254)

Estimated changes

modified theorem Nat.binCast_eq
modified theorem Nat.cast_add
modified theorem Nat.cast_bit0
modified theorem Nat.cast_bit1
modified theorem Nat.cast_eq_ofNat
modified theorem Nat.cast_ofNat
modified theorem Nat.cast_one
modified theorem Nat.cast_two
modified theorem one_add_one_eq_two
modified theorem three_add_one_eq_four
modified theorem two_add_one_eq_three