Commit 2025-07-02 10:10 fb81db9b

View on Github →

chore: rename the MonoidHomWithZero namespace to MonoidWithZeroHom (#26624) This seems to be a typo.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Range.lean

deleted theorem MonoidHomWithZero.inv_mem_valueGroup

deleted theorem MonoidHomWithZero.mem_valueGroup

deleted theorem MonoidHomWithZero.mem_valueGroup_iff_of_comm

deleted theorem MonoidHomWithZero.mem_valueMonoid

deleted theorem MonoidHomWithZero.mem_valueMonoid_iff

deleted def MonoidHomWithZero.valueGroup

deleted theorem MonoidHomWithZero.valueGroup_def

deleted theorem MonoidHomWithZero.valueGroup_eq_range

deleted def MonoidHomWithZero.valueMonoid

deleted theorem MonoidHomWithZero.valueMonoid_eq_closure

deleted theorem MonoidHomWithZero.valueMonoid_eq_valueGroup'

deleted theorem MonoidHomWithZero.valueMonoid_eq_valueGroup

added theorem MonoidWithZeroHom.inv_mem_valueGroup

added theorem MonoidWithZeroHom.mem_valueGroup

added theorem MonoidWithZeroHom.mem_valueGroup_iff_of_comm

added theorem MonoidWithZeroHom.mem_valueMonoid

added theorem MonoidWithZeroHom.mem_valueMonoid_iff

added def MonoidWithZeroHom.valueGroup

added theorem MonoidWithZeroHom.valueGroup_def

added theorem MonoidWithZeroHom.valueGroup_eq_range

added def MonoidWithZeroHom.valueMonoid

added theorem MonoidWithZeroHom.valueMonoid_eq_closure

added theorem MonoidWithZeroHom.valueMonoid_eq_valueGroup'

added theorem MonoidWithZeroHom.valueMonoid_eq_valueGroup

Modified Mathlib/RingTheory/Valuation/Discrete/Basic.lean