Commit 2025-08-14 21:19 7b983448

View on Github →

feat(Algebra/Order): ArchimedeanClass ball (#27885) Part of #27043 (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from #27451 (Valuation.ball) and Metric.ball / Metric.closedBall (ArchimedeanClass M actually becomes a Valuation when M is a ring so these names make sense).

Estimated changes

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

added theorem MulArchimedeanClass.ballSubgroup_antitone

added theorem MulArchimedeanClass.ballSubgroup_top

added theorem MulArchimedeanClass.closedBallSubgroup_top

added theorem MulArchimedeanClass.mem_ballSubgroup_iff

added theorem MulArchimedeanClass.mem_closedBallSubgroup_iff

added theorem MulArchimedeanClass.mem_subgroup_iff

added def MulArchimedeanClass.subgroup

added theorem MulArchimedeanClass.subgroup_antitone

added theorem MulArchimedeanClass.subgroup_eq_bot

added theorem MulArchimedeanClass.subgroup_strictAntiOn

added def MulArchimedeanClass.subsemigroup

added theorem MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top

Modified Mathlib/Order/UpperLower/Principal.lean

added theorem LowerSet.Iio_eq_bot

added theorem UpperSet.Ioi_eq_top