isUnramified_mk_iff — Mathlib

English

For a morphism φ with a conj relation, IsUnramified k (mk φ) iff σ = 1.

Русский

Для φ с отношением сопряжения IsUnramified k (mk φ) тогда и только тогда, σ = 1.

LaTeX

$$$IsUnramified\\; k\\; (mk\\; φ) \\iff σ = 1$$$

Lean4

theorem _root_.NumberField.ComplexEmbedding.IsConj.isUnramified_mk_iff {φ : K →+* ℂ} (h : ComplexEmbedding.IsConj φ σ) :
    IsUnramified k (mk φ) ↔ σ = 1 := by
  rw [h.ext_iff, ComplexEmbedding.isConj_one_iff, ← not_iff_not, not_isUnramified_iff, ← not_isReal_iff_isComplex,
    comap_mk, isReal_mk_iff, isReal_mk_iff, eq_true h.isReal_comp, and_true]

Похожие утверждения