Theorems · Theorem · commutative algebra

Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff

∀ {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 ∈ IsLocalRing.maximalIdeal ↥vL.valuationSubring ↔
    x ∈ IsLocalRing.maximalIdeal ↥vK.valuationSubring

Defined in

Mathlib.RingTheory.Valuation.Extension

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraLinearOrderedCommGroupWithZeroLinearOrderedCommGroupWithZeroValuation.HasExtension