Commit 2022-11-20 08:54 f04a595e

View on Github →

feat: Port Algebra.CharZero.Defs (#661) mathlib4 SHA 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CharZero/Defs.lean

added theorem Nat.cast_add_one_ne_zero

added theorem Nat.cast_eq_one

added theorem Nat.cast_eq_zero

added theorem Nat.cast_inj

added theorem Nat.cast_injective

added theorem Nat.cast_ne_one

added theorem Nat.cast_ne_zero

added theorem charZero_of_inj_zero