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
- instAlgebraWithVal_fLT v = inst✝
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
- instAlgebraWithVal_fLT_1 w = inst✝
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]
:
IsScalarTower A (WithVal v) 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]
:
IsScalarTower A B (WithVal w)