Theorems · Theorem · number theory

IsDecompositionField.algebraMap_ringEquiv_apply

∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (D : Type u_5) [inst_4 : Field D] [inst_5 : Algebra D L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (D' : Type u_8) [inst_7 : Field D'] [inst_8 : Algebra D' L]
  [inst_9 : IsDecompositionField K L P D] [inst_10 : IsDecompositionField K L P D'] (x : D),
  (algebraMap D' L) ((IsDecompositionField.ringEquiv K L P D D') x) = (algebraMap D L) x

Defined in

Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraCommRingFieldAlgebraMulSemiringActionFieldAlgebraIsDecompositionFieldIsDecompositionField