Commit 2026-01-16 16:52 c1313c03

View on Github →

refactor(Algebra/Order): change MulArchimedeanClass.subgroup to FiniteArchimedeanClass.subgroup (#32886) This gets rid of a junk value without much modification of the main HahnEmbedding application.

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean/Class.lean

added theorem FiniteMulArchimedeanClass.ballSubgroup_strictAnti

added theorem FiniteMulArchimedeanClass.mem_ballSubgroup_iff

added theorem FiniteMulArchimedeanClass.mem_closedBallSubgroup_iff

added theorem FiniteMulArchimedeanClass.mem_subgroup_iff

added theorem FiniteMulArchimedeanClass.min_le_mk_mul

added theorem FiniteMulArchimedeanClass.mk_inv

added def FiniteMulArchimedeanClass.subgroup

added theorem FiniteMulArchimedeanClass.subgroup_eq_bot

added theorem FiniteMulArchimedeanClass.subgroup_strictAnti

added theorem FiniteMulArchimedeanClass.subsemigroup_eq_subgroup

added def FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass

added theorem MulArchimedeanClass.subsemigroup_strictAnti

Modified Mathlib/Algebra/Order/Module/Archimedean.lean

added theorem FiniteArchimedeanClass.ball_lt_closedBall

added theorem FiniteArchimedeanClass.ball_strictAnti

added theorem FiniteArchimedeanClass.mem_ball_iff

added theorem FiniteArchimedeanClass.mem_closedBall_iff

added def FiniteArchimedeanClass.submodule

added theorem FiniteArchimedeanClass.submodule_strictAnti

added theorem FiniteArchimedeanClass.toAddSubgroup_ball

added theorem FiniteArchimedeanClass.toAddSubgroup_closedBall

Modified Mathlib/Algebra/Order/Module/HahnEmbedding.lean

deleted theorem HahnEmbedding.ArchimedeanStrata.ball_eq_closedBall

deleted theorem HahnEmbedding.ArchimedeanStrata.nontrivial_stratum

deleted theorem HahnEmbedding.ArchimedeanStrata.stratum_eq_bot_iff

added theorem HahnEmbedding.ArchimedeanStrata.stratum_ne_bot

deleted theorem HahnEmbedding.ArchimedeanStrata.stratum_top

modified theorem HahnEmbedding.Partial.mem_domain

added theorem HahnEmbedding.Partial.val_sub_ne_zero

modified def HahnEmbedding.Seed.coeff'

modified def HahnEmbedding.Seed.hahnCoeff

modified theorem HahnEmbedding.Seed.mem_domain_baseEmbedding