Structures · Algebra
LinearOrderedCommGroupWithZero
A linearly ordered commutative group with a zero element.
- Shape
- One type argument · adds div_eq_mul_inv, zpow_zero', zpow_succ', zpow_neg', inv_zero, mul_inv_cancel
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances9
- NNReal
- NNRat
- ValuativeRel.ValueGroupWithZero
- ValuationRing.ValueGroup
- ValuationSubring.ValueGroup
- MonoidWithZeroHom.ValueGroup₀
- Subtype
- Multiplicative
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by667
- Valuation.restrict
- Valuation.integer
- Valuation.valuationSubring
- WithVal.ofVal
- WithVal.equiv
- Valuation.Completion
- WithZeroTopology.topologicalSpace
- Valuation.IsRankOneDiscrete.generator
- Valued.integer
- Valuation.IsUniformizer
- Valuation.integer.integers
- Valuation.RankOne.hom
- Valuation.Integers.hom_inj
- ValuativeRel.ValueGroupWithZero.orderMonoidIso
- Valued.toNormedField
- WithVal.equiv_symm_apply
- MonoidWithZeroHom.ValueGroup₀.embedding_strictMono
- Valuation.ltAddSubgroup
- Valued.valuedCompletion_apply
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt
- Valuation.Uniformizer.val
- Valuation.RankOne.strictMono
- WithVal.congr
- Valuation.restrict_lt_iff_lt_embedding
- Valued.extensionValuation
- Valuation.Integers.exists_of_le_one
- Valuation.IsRankOneDiscrete.generator'
- Valuation.Integers.map_le_one
- Valuation.embedding_restrict
- Valuation.restrict_lt_iff
- Valuation.IsEquiv.orderMonoidIso
- Valuation.Integers.isUnit_iff_valuation_eq_one
- Valuation.restrict_def
- WithZeroTopology.nhds_of_ne_zero
- WithVal.valueGroupEquiv
- Valuation.norm
- WithVal.valueGroupOrderIso₀
- Valued.extension
- RatFunc.uniformizingPolynomial
- Valued.mem_nhds
- Valuation.leSubmodule
- Valuation.leIdeal
- ValuativeRel.ValueGroupWithZero.embed
- Valuation.restrict_le_one_iff
- Valued.hasBasis_nhds_zero
- WithVal.equiv_apply
- Valuation.mem_nhds_iff
- Valuation.restrict_le_iff
- Valuation.Integers.le_iff_dvd
- Valuation.Integers.coe_span_singleton_eq_setOfPred_le_v_algebraMap
Ancestors60
- Bot
- CommGroupWithZero
- CommMagma
- CommMonoid
- CommMonoidWithZero
- CommSemigroup
- DistribLattice
- Div
- DivInvMonoid
- DivInvOneMonoid
- DivisionCommMonoid
- DivisionMonoid
- Dvd
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- GroupWithZero
- HDiv
- HMul
- HSMul
- Inv
- InvOneClass
- InvolutiveInv
- IsBotZeroClass
- LE
- LT
- Lattice
- LinearOrder
- LinearOrderedCommMonoidWithZero
- Max
- Min
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NPow
- NSMul
- Nonempty
- Nontrivial
- OfNat
- One
- Ord
- OrderBot
- PartialOrder
- PosMulStrictMono
- Preorder
- SMul
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SemilatticeInf
- SemilatticeSup
- ZPow
- ZSMul
- Zero