Structures · Algebra
Valuation.HasExtension
The class Valuation.HasExtension vR vA states that the valuation vA on A is an extension of
the valuation vR on R. More precisely, vR is equivalent to the comap of the valuation vA.
- Defined in
- Mathlib.RingTheory.Valuation.Extension
- Shape
- 2 explicit arguments · adds val_isEquiv_comap
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- Valuation.HasExtension.val_map_le_iff
- Valuation.HasExtension.val_isEquiv_comap
- Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff
- Valuation.HasExtension.val_map_le_one_iff
- Valuation.HasExtension.coe_algebraMap_valuationSubring_eq
- Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap
- Valuation.HasExtension.val_map_eq_iff
- Valuation.HasExtension.instIsScalarTowerInteger
- Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal
- Valuation.HasExtension.instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap
- Valuation.HasExtension.val_smul
- Valuation.HasExtension.val_map_eq_one_iff
- Valuation.HasExtension.instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal
- Valuation.HasExtension.instIsTorsionFreeInteger
- Valuation.HasExtension.instAlgebraInteger
- Valuation.HasExtension.algebraMap_injective
- Valuation.HasExtension.algebraMap_mem_valuationSubring
- Valuation.HasExtension.val_map_lt_one_iff
- Valuation.HasExtension.instAlgebra_valuationSubring
- Valuation.HasExtension.instIsLocalHomValuationInteger
- Valuation.HasExtension.instIsScalarTower_valuationSubring'
- Valuation.HasExtension.val_algebraMap
- Valuation.HasExtension.val_map_lt_iff
- Valuation.HasExtension.mk_smul_mk
Ancestors0
No ancestors.