Theorem LinearOrderedCommGroup.Subgroup.genLTOne_mem

Modification history

2025-07-11 14:29
Mathlib/Algebra/Order/Group/Cyclic.lean
feat(RingTheory/Valuation/Discrete/Basic): add uniformizer API (#26591) …
Added LinearOrderedCommGroup.Subgroup.genLTOne_memView on Github →