Def FiniteMulArchimedeanClass.subgroup

Modification history

2026-02-17 23:08

Mathlib/Algebra/Order/Archimedean/Class.lean

chore: bump toolchain to v4.29.0-rc1 (#35459)

Deleted FiniteMulArchimedeanClass.subgroup View on Github →

2026-01-16 16:52

Mathlib/Algebra/Order/Archimedean/Class.lean

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

Added FiniteMulArchimedeanClass.subgroup View on Github →