Theorem MonoidWithZeroHom.mrange_nontrivial

Modification history

2025-07-15 08:11

Mathlib/Algebra/GroupWithZero/Range.lean

feat(Algebra/GroupWithZero/Range): MonoidWithZeroHom.(m)range_nontrivial (#27114) …

Added MonoidWithZeroHom.mrange_nontrivial View on Github →