Theorems · Theorem · commutative algebra

Valuation.HasExtension.coe_algebraMap_valuationSubring_eq

∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁) [inst_5 : vK.HasExtension vL]
  (x : ↥vK.valuationSubring), ↑((algebraMap ↥vK.valuationSubring ↥vL.valuationSubring) x) = (algebraMap K L) ↑x

Defined in

Mathlib.RingTheory.Valuation.Extension

Cited by

0 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraLinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZeroValuation.HasExtension