Documentation Verification Report

Range

📁 Source: Mathlib/Algebra/Order/GroupWithZero/Range.lean

Statistics

Metric	Count
Definitions `instLinearOrderedCommGroupWithZero`, `orderMonoidWithZeroHom`	2
Theorems `embedding_strictMono`, `embedding_unit_ne_zero`, `embedding_unit_pos`, `instIsOrderedMonoid`, `monoidWithZeroHom_strictMono`	5
Total	7

MonoidWithZeroHom.ValueGroup₀

Definitions

Name	Category	Theorems
`instLinearOrderedCommGroupWithZero` 📖	CompOp	74 math math: `Valuation.mem_nhds_zero_iff`, `Valued.isOpen_closedball`, `Valuation.isClopen_closedBall`, `Valued.extension_extends`, `WithVal.valueGroupOrderIso₀_restrict`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective`, `Valuation.restrict_eq_one_iff`, `Valuation.IsEquiv.restrict`, `Valued.isClopen_ball`, `Valuation.hasBasis_nhds_zero`, `Valuation.restrict_le_iff`, `Valued.is_topological_valuation`, `IsValuativeTopology.isOpen_ball`, `Valuation.restrict_eq_zero_iff`, `Valuation.restrict_eq_mk`, `Valued.continuous_valuation`, `Valuation.restrict_lt_iff_lt_embedding`, `IsValuativeTopology.isClopen_sphere`, `Valued.isOpen_sphere`, `Valuation.restrict_le_iff_le_embedding`, `Valuation.isEquiv_restrict`, `Valuation.RankOne.exists_val_lt`, `Valued.hasBasis_nhds_zero`, `Valued.coe_valuation_eq_rankOne_hom_comp_valuation`, `Valued.isClosed_ball`, `Valuation.restrict_lt_one_iff`, `Valued.isClopen_sphere`, `Valued.isClosed_sphere`, `IsValuativeTopology.isClosed_closedBall`, `Valuation.cauchy_iff`, `Valuation.restrict_inj`, `Valuation.embedding_restrict`, `Valued.valuation_isClosedMap`, `Valued.cauchy_iff`, `Valuation.restrict_pos_iff`, `IsValuativeTopology.isClopen_ball`, `Valuation.restrict_def`, `Valuation.isClosed_closedBall`, `IsValuativeTopology.isOpen_closedBall`, `Valuation.isClopen_ball`, `Valued.isOpen_closedBall`, `Valuation.hasBasis_nhds`, `Valued.mem_nhds_zero`, `Valuation.RankLeOne.exists_val_lt`, `Valued.isOpen_ball`, `Valued.mem_nhds`, `Valuation.isOpen_ball`, `IsValuativeTopology.isClosed_ball`, `WithVal.valueGroupOrderIso₀_symm_restrict`, `Valuation.hasBasis_uniformity`, `Valued.toNormedField.norm_def`, `Valuation.isOpen_sphere`, `Valuation.norm_def`, `Valuation.exists_div_eq_of_unit`, `Valuation.restrict_le_one_iff`, `Valuation.isClosed_ball`, `Valued.hasBasis_uniformity`, `ValuativeRel.valuation_lt_symm_orderMonoidIso`, `Valuation.restrict_lt_iff`, `Valued.isClosed_closedBall`, `Valuation.isOpen_closedBall`, `Valuation.RankOne.isNontrivial_restrict`, `ValuativeRel.restrict_lt_orderMonoidIso`, `Valuation.restrict_exists_div_eq`, `Valuation.IsEquiv.orderMonoidIso_spec`, `Valued.isClopen_closedBall`, `Valuation.RankOne.restrict_RankOne_hom_eq`, `Valuation.exists_setOf_restrict_le_iff`, `IsValuativeTopology.isOpen_sphere`, `IsValuativeTopology.isClopen_closedBall`, `Valuation.mem_nhds_iff`, `Valuation.is_topological_valuation`, `Valuation.isClopen_sphere`, `Valuation.isClosed_sphere`
`orderMonoidWithZeroHom` 📖	CompOp	1 math math: `monoidWithZeroHom_strictMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embedding_strictMono` 📖	mathematical	—	`StrictMono` `MonoidWithZeroHom.ValueGroup₀` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `MonoidWithZeroHom.funLike` `MonoidWithZeroHom.monoidWithZeroHomClass` `WithZero.instPreorder` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Subtype.preorder` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `WithZero.instMulZeroOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `embedding`	—	`MonoidWithZeroHom.monoidWithZeroHomClass` `OrderEmbedding.lt_iff_lt` `StrictMono.lt_iff_lt` `monoidWithZeroHom_strictMono`
`embedding_unit_ne_zero` 📖	—	—	—	—	`MonoidWithZeroHom.monoidWithZeroHomClass` `LT.lt.ne` `embedding_unit_pos`
`embedding_unit_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZeroHom.ValueGroup₀` `MonoidWithZeroHom.funLike` `MonoidWithZeroHom.monoidWithZeroHomClass` `WithZero.instMulZeroOneClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `embedding` `Units.val` `WithZero.instMonoidWithZero`	—	`MonoidWithZeroHom.monoidWithZeroHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `embedding_restrict₀` `StrictMono.lt_iff_lt` `embedding_strictMono`
`instIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `MonoidWithZeroHom.ValueGroup₀` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `MonoidWithZeroHom.funLike` `MonoidWithZeroHom.monoidWithZeroHomClass` `CommMonoidWithZero.toCommMonoid` `WithZero.instCommMonoidWithZero` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `CommGroup.toCommMonoid` `Subgroup.toCommGroup` `Units.instCommGroupUnits` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Subtype.preorder` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder`	—	`Function.Injective.isOrderedMonoid` `MonoidWithZeroHom.monoidWithZeroHomClass` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `StrictMono.le_iff_le` `embedding_strictMono`
`monoidWithZeroHom_strictMono` 📖	mathematical	—	`StrictMono` `MonoidWithZeroHom.ValueGroup₀` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `MonoidWithZeroHom.funLike` `MonoidWithZeroHom.monoidWithZeroHomClass` `WithZero` `Units` `MonoidWithZero.toMonoid` `WithZero.instPreorder` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Subtype.preorder` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `OrderMonoidWithZeroHom` `WithZero.instMulZeroOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Units.instMulOneClass` `OrderMonoidWithZeroHom.instFunLike` `orderMonoidWithZeroHom`	—	`WithZero.map'_strictMono` `MonoidWithZeroHom.monoidWithZeroHomClass` `Subtype.strictMono_coe`

---

← Back to Index