Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-21 18:58 217b5e72

View on Github →

refactor(algebra/char_zero): use function.injective (#1894) No need to require ↔ in the definition.

Estimated changes

Modified src/algebra/char_zero.lean

modified theorem nat.cast_eq_zero

modified theorem nat.cast_injective

modified theorem nat.cast_ne_zero

Modified src/data/padics/padic_numbers.lean

Modified src/data/real/ennreal.lean

added theorem ennreal.coe_nat_le_coe_nat

modified theorem ennreal.coe_nat_lt_coe_nat

added theorem ennreal.coe_nat_mono

Modified src/data/zsqrtd/basic.lean