Commit 2025-12-08 11:36 e10075ac

View on Github →

feat(Algebra/Group/Indicator): generalize MonoidHom to OneHomClass (#32575) This PR generalizesMonoidHom.map_mulIndicator to map_mulIndicator that works for any f : F where OneHomClass F.

Estimated changes

Modified Mathlib/Algebra/Group/Indicator.lean

deleted theorem MonoidHom.map_mulIndicator

added theorem map_mulIndicator

Modified Mathlib/Data/ENNReal/Lemmas.lean

Modified Mathlib/Data/NNRat/Lemmas.lean

Modified Mathlib/Data/NNReal/Basic.lean