Structures · Algebra
Valuation.IsNontrivial
A valuation on a ring is nontrivial if there exists an element with valuation
not equal to 0 or 1.
- Defined in
- Mathlib.RingTheory.Valuation.Basic
- Shape
- One type argument · adds exists_val_nontrivial
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- RatFunc
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- RatFunc.uniformizingPolynomial
- RatFunc.valuationIdeal
- Valuation.IsNontrivial.exists_lt_one
- RatFunc.setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty
- RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one
- Valuation.IsNontrivial.exists_val_nontrivial
- RatFunc.uniformizingPolynomial_ne_zero
- Valued.integer.isDiscreteValuationRing_of_compactSpace
- Valuation.nonempty_rankOne_iff_mulArchimedean
- RatFunc.uniformizingPolynomial_isUniformizer
- RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one
- RatFunc.valuation_uniformizingPolynomial_lt_one
- Valuation.IsNontrivial.exists_one_lt
- RatFunc.exists_zpow_uniformizingPolynomial
- Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfClassOfIsNontrivial
- Valuation.IsNontrivial.nontrivial_codomain
- RatFunc.valuationIdeal.congr_simp
- RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty
- RatFunc.uniformizingPolynomial.congr_simp
- Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfClassOfIsNontrivial
Ancestors0
No ancestors.