Commit 2024-07-27 19:36 ed41c0c5

View on Github →

feat: OfNat.ofNat n • x = n • x and Nat.cast n • x = n • x (#14997)

Estimated changes

deleted theorem intCast_smul
added theorem Int.cast_smul_eq_nsmul
added theorem Nat.cast_smul_eq_nsmul
modified theorem Nat.noZeroSMulDivisors
modified theorem int_smul_eq_zsmul
modified theorem nat_smul_eq_nsmul
modified theorem nsmul_eq_smul_cast
added theorem ofNat_smul_eq_nsmul
modified theorem zsmul_eq_smul_cast