Structures · Algebra
Valuation.IsRankOneDiscrete
Given a linearly ordered commutative group with zero Γ such that Γˣ is
nontrivial cyclic, a valuation v : A → Γ on a ring A is discrete, if
genLTOne Γˣ belongs to the image. Note that the latter is equivalent to
asking that 1 : ℤ belongs to the image of the corresponding additive valuation.
- Shape
- One type argument · adds exists_generator_lt_one'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by58
- Valuation.IsRankOneDiscrete.generator
- Valuation.IsUniformizer
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt
- Valuation.Uniformizer.val
- Valuation.IsRankOneDiscrete.generator'
- Valuation.Uniformizer.is_generator
- Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator
- Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup
- Valuation.Uniformizer.valuation_gt_one
- Valuation.IsRankOneDiscrete.generator_lt_one
- Valuation.IsUniformizer.ne_zero
- Valuation.IsRankOneDiscrete.generator'_zpowers_eq_top
- Valuation.IsUniformizer.val
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply
- Valuation.IsUniformizer.iff
- Valuation.IsRankOneDiscrete.exists_generator_lt_one
- Valuation.exists_pow_Uniformizer
- Valuation.IsUniformizer.val_lt_one
- Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_surjective
- Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range
- Valuation.IsUniformizer.not_isUnit
- Valuation.IsUniformizer.val_ne_zero
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective
- Valuation.IsUniformizer.zpowers_eq_valueGroup
- RatFunc.valuation_isEquiv_infty_or_adic
- Valuation.IsUniformizer.congr_simp
- Valuation.Uniformizer.ne_zero
- RatFunc.uniformizingPolynomial_isUniformizer
- Valuation.IsUniformizer.of_associated
- Valuation.IsRankOneDiscrete.generator'_lt_one
- RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one
- RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one
- Valuation.IsRankOneDiscrete.generator_mem_valueGroup
- Valuation.IsRankOneDiscrete.generator_zpowers_eq_range
- Valuation.IsRankOneDiscrete.exists_generator_lt_one'
- Valuation.IsUniformizer.val_pos
- Valuation.IsUniformizer.is_generator
- Valuation.IsRankOneDiscrete.generator_ne_one
- Valuation.isUniformizer_of_maximalIdeal_eq_span
- Valuation.pow_Uniformizer_is_pow_generator
- Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjective
- Valuation.IsRankOneDiscrete.rankOne
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt.congr_simp
- Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroupOfClass
- Valuation.IsRankOneDiscrete.generator_ne_zero
- Valuation.IsRankOneDiscrete.generator'.congr_simp
- RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty
- Valuation.IsRankOneDiscrete.generator_mem_range
- Valuation.IsRankOneDiscrete.instIsNontrivial
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow
Ancestors0
No ancestors.