Theorem MonoidWithZeroHom.one_mem_valueMonoid

Modification history

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.one_mem_valueMonoidView on Github →