Theorem HahnEmbedding.Partial.val_sub_ne_zero

Modification history

2026-01-16 16:52
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
refactor(Algebra/Order): change `MulArchimedeanClass.subgroup` to `FiniteArchimedeanClass.subgroup` (#32886) …
Added HahnEmbedding.Partial.val_sub_ne_zeroView on Github →