Def FiniteArchimedeanClass.submodule

Modification history

2026-01-16 16:52

Mathlib/Algebra/Order/Module/Archimedean.lean

refactor(Algebra/Order): change `MulArchimedeanClass.subgroup` to `FiniteArchimedeanClass.subgroup` (#32886) …

Added FiniteArchimedeanClass.submodule View on Github →