Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-25 13:19 4d761f44

View on Github →

feat(algebra/group/hom): Notation for monoid_with_zero_hom (#11632) Introduce notation →*₀ for monoid_with_zero_hom and use it everywhere.

Estimated changes

modified def normalize
modified theorem monoid_with_zero_hom.ext
modified theorem monoid_with_zero_hom.mk_coe
modified theorem abs_div
modified theorem abs_inv
modified def abs_hom
modified def quaternion.norm_sq
modified theorem normed_field.nnnorm_div
modified theorem normed_field.norm_div
modified def normed_field.norm_hom
modified theorem normed_field.norm_inv
modified theorem normed_field.norm_zpow
modified def complex.norm_sq
modified def is_R_or_C.norm_sq
modified theorem valuation.coe_coe
modified theorem valuation.is_equiv.map
modified def valuation.map
modified structure valuation