Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-19 09:07 272e2d22

View on Github →

feat(data/{int, nat, rat}/cast): extensionality lemmas (#6788) Extensionality lemmas

Estimated changes

Modified src/algebra/group_power/lemmas.lean

deleted theorem monoid_hom.ext_mint

Modified src/data/int/cast.lean

modified theorem monoid_hom.ext_int

added theorem monoid_hom.ext_mint

added theorem monoid_with_zero_hom.ext_int'

added theorem monoid_with_zero_hom.ext_int

Modified src/data/nat/cast.lean

added theorem monoid_with_zero_hom.ext_nat

Modified src/data/rat/cast.lean

added theorem monoid_with_zero_hom.ext_rat

added theorem monoid_with_zero_hom.ext_rat_on_pnat