Structures · Algebra
Valuation.IsTrivialOn
A valuation on an A-algebra B is trivial on constants if the nonzero elements of the
base ring A are mapped to 1.
This is true, for example, when A is a finite field.
See Valuation.FiniteField.instIsTrivialOn.
- Defined in
- Mathlib.RingTheory.Valuation.Basic
- Shape
- 2 explicit arguments · adds eq_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 by27
- RatFunc.uniformizingPolynomial
- Valuation.IsTrivialOn.eq_one
- RatFunc.valuationIdeal
- RatFunc.setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty
- Polynomial.valuation_le_one_of_valuation_X_le_one
- RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one
- Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X
- RatFunc.uniformizingPolynomial_ne_zero
- RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X
- RatFunc.valuation_isEquiv_infty_or_adic
- RatFunc.uniformizingPolynomial_isUniformizer
- RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one
- RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one
- Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X
- RatFunc.valuation_uniformizingPolynomial_lt_one
- Polynomial.valuation_aeval_monomial_eq_valuation_pow
- RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X
- RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero
- RatFunc.exists_zpow_uniformizingPolynomial
- Valuation.transcendental_of_ne_one
- Polynomial.valuation_inv_monomial_eq_valuation_X_zpow
- Polynomial.valuation_monomial_eq_valuation_X_pow
- Valuation.IsTrivialOn.valuation_algebraMap_le_one
- RatFunc.valuationIdeal.congr_simp
- RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty
- RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty
- RatFunc.uniformizingPolynomial.congr_simp
Ancestors0
No ancestors.