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	2 math math: `instAddArchimedean`, `isOrderedAddMonoid`
`instPreorder` 📖	CompOp	3 math math: `orderEmbeddingVal_apply`, `val_le_val`, `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: `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `instMulArchimedean`, `mulArchimedean_iff`, `isOrderedMonoid`
`instPreorder` 📖	CompOp	47 math math: `WithZero.logOrderIso_apply`, `Valuation.IsRankOneDiscrete.generator_lt_one`, `OrderMonoidIso.val_inv_unitsWithZero_symm_apply`, `WithZero.val_expOrderIso_apply`, `Valuation.IsRankOneDiscrete.exists_generator_lt_one'`, `OrderMonoidIso.val_unitsCongr_symm_apply`, `LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex`, `MonoidWithZeroHom.fst_mono`, `Valuation.ltAddSubgroup_monotone`, `WithZero.expOrderIso_symm_apply`, `OrderMonoidIso.val_unitsCongr_apply`, `OrderMonoidIso.val_inv_unitsCongr_symm_apply`, `orderEmbeddingVal_apply`, `OrderMonoidIso.withZeroUnits_symm_apply`, `MonoidWithZeroHom.inl_strictMono`, `OrderMonoidIso.withZeroUnits_apply`, `OrderMonoidIso.val_unitsWithZero_symm_apply`, `denselyOrdered_units_iff`, `OrderIso.withZeroUnits_symm_apply`, `WithZero.withZeroUnitsEquiv_symm_strictMono`, `val_le_val`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `OrderMonoidIso.unitsWithZero_apply`, `WithZero.val_inv_expOrderIso_apply`, `OrderMonoidIso.val_inv_unitsCongr_apply`, `Valuation.ltSubmodule_monotone`, `MonoidWithZeroHom.inr_mono`, `CStarAlgebra.one_le_inv_iff_le_one`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `LinearOrderedCommGroupWithZero.fst_comp_inl`, `MonoidWithZeroHom.snd_mono`, `Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer`, `LinearOrderedCommGroupWithZero.fst_apply`, `OrderIso.withZeroUnits_apply`, `MonoidWithZeroHom.inr_strictMono`, `MonoidWithZeroHom.inl_mono`, `val_lt_val`, `Valuation.ltIdeal_mono`, `LinearOrderedCommGroupWithZero.inl_apply`, `LinearOrderedCommGroupWithZero.inr_apply`, `denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units`, `Valuation.IsRankOneDiscrete.exists_generator_lt_one`, `WithZero.val_logOrderIso_symm_apply`, `CStarAlgebra.inv_le_one_iff_one_le`, `WithZero.val_inv_logOrderIso_symm_apply`, `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