Documentation Verification Report

Units

📁 Source: Mathlib/Algebra/Order/Monoid/Units.lean

Statistics

Metric	Count
Definitions `instLinearOrder`, `instMaxOfLinearOrder`, `instMinOfLinearOrder`, `instOrd`, `instPartialOrderAddUnits`, `instPreorder`, `orderEmbeddingVal`, `instLinearOrder`, `instMaxOfLinearOrder`, `instMinOfLinearOrder`, `instOrd`, `instPartialOrderUnits`, `instPreorder`, `orderEmbeddingVal`	14
Theorems `compare_val`, `max_val`, `min_val`, `orderEmbeddingVal_apply`, `val_le_val`, `val_lt_val`, `compare_val`, `max_val`, `min_val`, `orderEmbeddingVal_apply`, `val_le_val`, `val_lt_val`	12
Total	26

AddUnits

Definitions

Name	Category	Theorems
`instLinearOrder` 📖	CompOp	—
`instMaxOfLinearOrder` 📖	CompOp	1 math math: `max_val`
`instMinOfLinearOrder` 📖	CompOp	1 math math: `min_val`
`instOrd` 📖	CompOp	1 math math: `compare_val`
`instPartialOrderAddUnits` 📖	CompOp	1 math math: `instAddArchimedean`
`instPreorder` 📖	CompOp	4 math math: `orderEmbeddingVal_apply`, `val_le_val`, `isOrderedAddMonoid`, `val_lt_val`
`orderEmbeddingVal` 📖	CompOp	1 math math: `orderEmbeddingVal_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compare_val` 📖	mathematical	—	`val` `AddUnits` `instOrd`	—	—
`max_val` 📖	mathematical	—	`val` `AddUnits` `instMaxOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`max_def` `val_le_val`
`min_val` 📖	mathematical	—	`val` `AddUnits` `instMinOfLinearOrder` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`min_def` `val_le_val`
`orderEmbeddingVal_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `AddUnits` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelEmbedding.instFunLike` `orderEmbeddingVal` `val`	—	—
`val_le_val` 📖	mathematical	—	`Preorder.toLE` `val` `AddUnits` `instPreorder`	—	—
`val_lt_val` 📖	mathematical	—	`Preorder.toLT` `val` `AddUnits` `instPreorder`	—	—

Units

Definitions

Name	Category	Theorems
`instLinearOrder` 📖	CompOp	1 math math: `Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator`
`instMaxOfLinearOrder` 📖	CompOp	1 math math: `max_val`
`instMinOfLinearOrder` 📖	CompOp	1 math math: `min_val`
`instOrd` 📖	CompOp	1 math math: `compare_val`
`instPartialOrderUnits` 📖	CompOp	5 math math: `Valuation.nonempty_rankOne_iff_mulArchimedean`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `instMulArchimedean`, `mulArchimedean_iff`
`instPreorder` 📖	CompOp	116 math math: `Valuation.mem_nhds_zero_iff`, `WithZero.logOrderIso_apply`, `Valuation.IsRankOneDiscrete.generator_lt_one`, `Valued.isOpen_closedball`, `OrderMonoidIso.val_inv_unitsWithZero_symm_apply`, `WithZero.val_expOrderIso_apply`, `WithVal.valueGroupOrderIso₀_symm_apply`, `Valuation.isClopen_closedBall`, `Valuation.IsRankOneDiscrete.exists_generator_lt_one'`, `WithVal.valueGroupOrderIso₀_restrict`, `OrderMonoidIso.val_unitsCongr_symm_apply`, `MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono`, `WithVal.valueGroupOrderIso₀_apply`, `LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex`, `Valuation.IsRankOneDiscrete.generator'_lt_one`, `MonoidWithZeroHom.fst_mono`, `Valuation.ltAddSubgroup_monotone`, `Valued.isClopen_ball`, `ValuativeRel.ValueGroupWithZero.embed_strictMono`, `Valuation.hasBasis_nhds_zero`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀`, `WithZero.expOrderIso_symm_apply`, `Valuation.restrict_le_iff`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono`, `Valued.is_topological_valuation`, `IsValuativeTopology.isOpen_ball`, `OrderMonoidIso.val_unitsCongr_apply`, `ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso`, `Valuation.restrict_lt_iff_lt_embedding`, `OrderMonoidIso.val_inv_unitsCongr_symm_apply`, `orderEmbeddingVal_apply`, `OrderMonoidIso.withZeroUnits_symm_apply`, `MonoidWithZeroHom.inl_strictMono`, `OrderMonoidIso.withZeroUnits_apply`, `Valuation.restrict_le_iff_le_embedding`, `OrderMonoidIso.val_unitsWithZero_symm_apply`, `denselyOrdered_units_iff`, `OrderIso.withZeroUnits_symm_apply`, `Valued.hasBasis_nhds_zero`, `WithZero.withZeroUnitsEquiv_symm_strictMono`, `WithVal.strictMono_valueGroupOrderIso₀`, `WithVal.strictMono_valueGroupOrderIso₀_symm`, `val_le_val`, `Valuation.RankOne.strictMono`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk`, `Valued.isClosed_ball`, `Valuation.restrict_lt_one_iff`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `OrderMonoidIso.unitsWithZero_apply`, `IsValuativeTopology.isClosed_closedBall`, `WithZero.val_inv_expOrderIso_apply`, `Valuation.cauchy_iff`, `OrderMonoidIso.val_inv_unitsCongr_apply`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed`, `Valuation.ltSubmodule_monotone`, `Valued.cauchy_iff`, `MonoidWithZeroHom.inr_mono`, `CStarAlgebra.one_le_inv_iff_le_one`, `Valuation.restrict_pos_iff`, `IsValuativeTopology.isClopen_ball`, `Valuation.IsEquiv.orderMonoidIso_trans`, `WithVal.strictMono_valueGroupEquiv_symm`, `Valuation.isClosed_closedBall`, `IsValuativeTopology.isOpen_closedBall`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `LinearOrderedCommGroupWithZero.fst_comp_inl`, `MonoidWithZeroHom.snd_mono`, `Valuation.isClopen_ball`, `Valued.isOpen_closedBall`, `Valuation.hasBasis_nhds`, `Valued.mem_nhds_zero`, `Valued.isOpen_ball`, `Valued.mem_nhds`, `Valuation.isOpen_ball`, `Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer`, `IsValuativeTopology.isClosed_ball`, `LinearOrderedCommGroupWithZero.fst_apply`, `WithVal.valueGroupOrderIso₀_symm_restrict`, `ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq`, `Valuation.hasBasis_uniformity`, `Valuation.restrict_le_one_iff`, `Valuation.isClosed_ball`, `OrderIso.withZeroUnits_apply`, `Valuation.IsEquiv.orderMonoidIso_eq_refl`, `MonoidWithZeroHom.inr_strictMono`, `Valued.hasBasis_uniformity`, `ValuativeRel.valuation_lt_symm_orderMonoidIso`, `Valuation.restrict_lt_iff`, `Valued.isClosed_closedBall`, `Valuation.isOpen_closedBall`, `MonoidWithZeroHom.inl_mono`, `val_lt_val`, `ValuativeRel.restrict_lt_orderMonoidIso`, `Valuation.ltIdeal_mono`, `Valuation.IsEquiv.orderMonoidIso_spec`, `Valued.isClopen_closedBall`, `LinearOrderedCommGroupWithZero.inl_apply`, `LinearOrderedCommGroupWithZero.inr_apply`, `WithVal.strictMono_valueGroupEquiv`, `MonoidWithZeroHom.ValueGroup₀.instIsOrderedMonoid`, `Valuation.RankLeOne.strictMono'`, `denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units`, `Valuation.exists_setOf_restrict_le_iff`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono`, `Valuation.IsRankOneDiscrete.exists_generator_lt_one`, `isOrderedMonoid`, `WithZero.val_logOrderIso_symm_apply`, `MonoidWithZeroHom.ValueGroup₀.embedding_strictMono`, `CStarAlgebra.inv_le_one_iff_one_le`, `WithZero.val_inv_logOrderIso_symm_apply`, `IsValuativeTopology.isClopen_closedBall`, `Valuation.mem_nhds_iff`, `Valuation.is_topological_valuation`, `Valuation.IsEquiv.orderMonoidIso_symm`, `WithZero.withZeroUnitsEquiv_strictMono`, `instDenselyOrderedUnits`
`orderEmbeddingVal` 📖	CompOp	1 math math: `orderEmbeddingVal_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compare_val` 📖	mathematical	—	`val` `Units` `instOrd`	—	—
`max_val` 📖	mathematical	—	`val` `Units` `instMaxOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`max_def`
`min_val` 📖	mathematical	—	`val` `Units` `instMinOfLinearOrder` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`min_def`
`orderEmbeddingVal_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Units` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelEmbedding.instFunLike` `orderEmbeddingVal` `val`	—	—
`val_le_val` 📖	mathematical	—	`Preorder.toLE` `val` `Units` `instPreorder`	—	—
`val_lt_val` 📖	mathematical	—	`Preorder.toLT` `val` `Units` `instPreorder`	—	—

---

← Back to Index