Documentation

FLT.Mathlib.Topology.Algebra.Valued.WithVal

instance instAlgebraWithVal_fLT {K : Type u_2} {L : Type u_3} {Γ₀ : Type u_5} [Ring L] [CommRing K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) [Algebra K L] :
Equations
instance instAlgebraWithVal_fLT_1 {K : Type u_2} {L : Type u_3} {Γ₀ : Type u_5} [Ring L] [CommRing K] [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation L Γ₀) [Algebra K L] :
Equations
instance instIsScalarTowerWithVal_fLT {A : Type u_1} {K : Type u_2} {L : Type u_3} {Γ₀ : Type u_5} [Ring L] [CommRing K] [LinearOrderedCommGroupWithZero Γ₀] [Semiring A] [Module A K] [Module A L] (v : Valuation K Γ₀) [Algebra K L] [IsScalarTower A K L] :
instance instIsScalarTowerWithVal_fLT_1 {A : Type u_1} {L : Type u_3} {B : Type u_4} {Γ₀ : Type u_5} [Ring L] [LinearOrderedCommGroupWithZero Γ₀] [Semiring A] [Module A L] [Semiring B] [Module A B] [Module B L] (w : Valuation L Γ₀) [IsScalarTower A B L] :