Documentation Verification Report

Archimedean

📁 Source: Mathlib/Algebra/Order/Module/Archimedean.lean

Statistics

Metric	Count
Definitions `ball`, `closedBall`, `submodule`, `ball`, `closedBall`, `submodule`	6
Theorems `ball_antitone`, `ball_le_closedBall`, `ball_top`, `closedBall_top`, `mem_ball_iff`, `mem_closedBall_iff`, `mk_le_mk_smul`, `mk_smul`, `toAddSubgroup_ball`, `toAddSubgroup_closedBall`, `ball_lt_closedBall`, `ball_strictAnti`, `mem_ball_iff`, `mem_closedBall_iff`, `submodule_strictAnti`, `toAddSubgroup_ball`, `toAddSubgroup_closedBall`	17
Total	23

ArchimedeanClass

Definitions

Name	Category	Theorems
`ball` 📖	CompOp	5 math math: `mem_ball_iff`, `ball_le_closedBall`, `ball_top`, `toAddSubgroup_ball`, `ball_antitone`
`closedBall` 📖	CompOp	4 math math: `ball_le_closedBall`, `mem_closedBall_iff`, `closedBall_top`, `toAddSubgroup_closedBall`
`submodule` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_antitone` 📖	mathematical	—	`Antitone` `ArchimedeanClass` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `Submodule.instPartialOrder` `ball`	—	`Submodule.toAddSubgroup_le` `ballAddSubgroup_antitone`
`ball_le_closedBall` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `ball` `closedBall`	—	`eq_or_ne` `ball_top` `closedBall_top` `LT.lt.le` `mem_ball_iff`
`ball_top` 📖	mathematical	—	`ball` `Top.top` `ArchimedeanClass` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `instOrderTop` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	—	`ballAddSubgroup_top`
`closedBall_top` 📖	mathematical	—	`closedBall` `Top.top` `ArchimedeanClass` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `instOrderTop` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	—	`closedBallAddSubgroup_top`
`mem_ball_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `ball` `ArchimedeanClass` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`mem_ballAddSubgroup_iff`
`mem_closedBall_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `closedBall` `ArchimedeanClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`mem_closedBallAddSubgroup_iff`
`mk_le_mk_smul` 📖	mathematical	—	`ArchimedeanClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`eq_or_ne` `zero_smul` `mk_smul`
`mk_smul` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`nontrivial_iff` `Archimedean.arch` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `abs_smul` `smul_assoc` `AddCommMonoid.nat_isScalarTower` `le_smul_of_one_le_left` `PosSMulMono.toSMulPosMono` `covariant_swap_add_of_covariant_add` `one_smul` `smul_le_smul_of_nonneg_right`
`toAddSubgroup_ball` 📖	mathematical	—	`Submodule.toAddSubgroup` `ball` `ballAddSubgroup`	—	—
`toAddSubgroup_closedBall` 📖	mathematical	—	`Submodule.toAddSubgroup` `closedBall` `closedBallAddSubgroup`	—	—

FiniteArchimedeanClass

Definitions

Name	Category	Theorems
`ball` 📖	CompOp	7 math math: `ball_lt_closedBall`, `toAddSubgroup_ball`, `HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq`, `HahnEmbedding.Partial.exists_sub_mem_ball`, `HahnEmbedding.ArchimedeanStrata.disjoint_ball_stratum`, `mem_ball_iff`, `ball_strictAnti`
`closedBall` 📖	CompOp	4 math math: `ball_lt_closedBall`, `HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq`, `toAddSubgroup_closedBall`, `mem_closedBall_iff`
`submodule` 📖	CompOp	1 math math: `submodule_strictAnti`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_lt_closedBall` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `ball` `closedBall`	—	`submodule_strictAnti` `Set.Ioi_ssubset_Ici_self`
`ball_strictAnti` 📖	mathematical	—	`StrictAnti` `FiniteArchimedeanClass` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Subtype.preorder` `ArchimedeanClass` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `ArchimedeanClass.instOrderTop` `Submodule.instPartialOrder` `ball`	—	`ballAddSubgroup_strictAnti`
`mem_ball_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `ball` `FiniteArchimedeanClass` `ArchimedeanClass` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `ArchimedeanClass.instOrderTop`	—	`mem_ballAddSubgroup_iff`
`mem_closedBall_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `closedBall` `FiniteArchimedeanClass` `ArchimedeanClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `ArchimedeanClass.instOrderTop`	—	`mem_closedBallAddSubgroup_iff`
`submodule_strictAnti` 📖	mathematical	—	`StrictAnti` `UpperSet` `FiniteArchimedeanClass` `ArchimedeanClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `ArchimedeanClass.instOrderTop` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `UpperSet.instPartialOrder` `Submodule.instPartialOrder` `submodule`	—	`addSubgroup_strictAnti`
`toAddSubgroup_ball` 📖	mathematical	—	`Submodule.toAddSubgroup` `ball` `ballAddSubgroup`	—	—
`toAddSubgroup_closedBall` 📖	mathematical	—	`Submodule.toAddSubgroup` `closedBall` `closedBallAddSubgroup`	—	—

---

← Back to Index