Theorems · Theorem · commutative algebra

Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap

∀ {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 (IsLocalRing.ResidueField ↥vK.valuationSubring) (IsLocalRing.ResidueField ↥vL.valuationSubring))
      ((IsLocalRing.residue ↥vK.valuationSubring) x) =
    (IsLocalRing.residue ↥vL.valuationSubring) ((algebraMap ↥vK.valuationSubring ↥vL.valuationSubring) x)

Defined in

Mathlib.RingTheory.Valuation.Extension

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraLinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZeroValuation.HasExtension