Theorem MonoidWithZeroHom.coe_one

Modification history

2025-07-16 20:44
Mathlib/Algebra/GroupWithZero/Range.lean
chore: tidy various files (#27220)
Modified MonoidWithZeroHom.coe_oneView on Github →
2025-07-10 14:00
Mathlib/Algebra/GroupWithZero/Range.lean
feat(RingTheory/Valuation/Discrete/Basic.lean): add Nontriviality instances for discrete valuations (#26587) …
Added MonoidWithZeroHom.coe_oneView on Github →