Commit 2022-12-13 23:46 be3b492c

View on Github →

feat: port Data.Nat.Cast.Basic (#980) mathlib3 SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e STATUS: Finished, except for porting Pi.addMonoidWithOne. See this Zulip thread Another issue during the port

Estimated changes

added theorem Nat.cast_pow
added theorem AddMonoidHom.ext_nat
added theorem MulOpposite.op_natCast
added theorem Nat.StrictMono_cast
added theorem Nat.abs_cast
added def Nat.castRingHom
added theorem Nat.castRingHom_nat
added theorem Nat.cast_add_one_pos
added theorem Nat.cast_comm
modified theorem Nat.cast_commute
modified theorem Nat.cast_id
added theorem Nat.cast_le
added theorem Nat.cast_le_one
added theorem Nat.cast_lt
added theorem Nat.cast_lt_one
added theorem Nat.cast_max
added theorem Nat.cast_min
modified theorem Nat.cast_mul
added theorem Nat.cast_nonneg
added theorem Nat.cast_pos
deleted theorem Nat.cast_pow
added theorem Nat.cast_tsub
added theorem Nat.coe_castRingHom
added theorem Nat.coe_nat_dvd
added theorem Nat.commute_cast
added theorem Nat.mono_cast
added theorem Nat.one_le_cast
added theorem Nat.one_lt_cast
added theorem NeZero.nat_of_ne_zero
added theorem Pi.coe_nat
added theorem Pi.nat_apply
added theorem RingHom.eq_natCast'
added theorem eq_natCast'
added theorem eq_natCast
added theorem ext_nat''
added theorem ext_nat'
added theorem ext_nat
added theorem map_natCast'
added theorem map_natCast
added theorem ofDual_natCast
added theorem ofLex_natCast
added theorem toDual_natCast
added theorem toLex_natCast