Commit 2026-09-16 13:44 4075d732

View on Github →

fix(Algebra/MonoidWithZeroHom): normalize to .toMonoidWithZeroHom (#43728) As discussed in #mathlib4 > Mathlib's morphism hierarchy, this PR fixes the normalization direction from .ofClass f to f.toMonoidWithZeroHom.

Estimated changes

modified theorem AddValuation.IsEquiv.map
modified def AddValuation.map
modified theorem AddValuation.map_apply
modified theorem Valuation.IsEquiv.map
deleted theorem Valuation.coe_ofClass
modified def Valuation.comap
modified def Valuation.map
modified theorem Valuation.map_apply
added theorem Valuation.map_comp
modified def Valuation.restrict
modified theorem Valuation.restrict_def
modified theorem Valuation.restrict_eq_mk
modified theorem Valuation.ideal_isPrincipal
modified theorem Valuation.isClopen_ball
modified theorem Valuation.isClopen_sphere
modified theorem Valuation.isClosed_ball
modified theorem Valuation.isClosed_sphere
modified theorem Valuation.isOpen_ball
modified theorem Valuation.isOpen_closedBall
modified theorem Valuation.isOpen_sphere
modified theorem Valued.isClopen_ball
modified theorem Valued.isClopen_closedBall
modified theorem Valued.isClopen_sphere
modified theorem Valued.isClosed_ball
modified theorem Valued.isClosed_closedBall
modified theorem Valued.isClosed_sphere
modified theorem Valued.isOpen_ball
modified theorem Valued.isOpen_closedBall
modified theorem Valued.isOpen_sphere
modified theorem WithVal.valueGroup_eq