Commit 2023-02-20 08:33 5c82b503

View on Github →

feat: simplify equality of nat literals (#2389) If M has characteristic zero, then we simplify, e.g., (2 : M) = 10 to (2 : ℕ) = 10.

Estimated changes

Modified Mathlib/Algebra/CharZero/Defs.lean

added theorem OfNat.ofNat_eq_ofNat

added theorem OfNat.ofNat_ne_one

added theorem OfNat.ofNat_ne_zero

added theorem OfNat.one_ne_ofNat

added theorem OfNat.zero_ne_ofNat

Modified Mathlib/Data/Nat/Cast/Defs.lean

added theorem Nat.cast_eq_ofNat