Commit 2026-03-02 10:51 32025af6

feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range (#26588) We extend the embedding of the range of a MonoidWithZeroHom to the codomain by enriching it with the structure of an ordered, multiplicative embedding. In passing, we extend some results about the embedding of WithZero of the units of a group with zero, to the group itself. This will be used in the theory on valuation on rings. In particular, it is needed for correcting the definition of Valuation.IsRankOne in Mathlib (see #26872).