not_isUnramified_iff — Mathlib

English

Not unramified iff w is complex and the real-ness of the comap place holds (i.e., real vs complex relationship).

Русский

Не неразмороженность эквивалентна тому, что w комплексное место и comap-положение реальное.

LaTeX

$$$\\neg IsUnramified\\; k\\; w \\iff (IsComplex w \\wedge IsReal (w.comap (algebraMap k K)))$$$

Lean4

/-- An infinite place is not unramified (i.e. ramified) iff it is a complex place above a real place.
-/
theorem not_isUnramified_iff : ¬IsUnramified k w ↔ IsComplex w ∧ IsReal (w.comap (algebraMap k K)) :=
  by
  rw [IsUnramified, mult, mult, ← not_isReal_iff_isComplex]
  split_ifs with h₁ h₂ h₂ <;>
    simp only [not_true_eq_false, false_iff, and_self, forall_true_left, IsEmpty.forall_iff, not_and,
      OfNat.one_ne_ofNat, not_false_eq_true, true_iff, OfNat.ofNat_ne_one, h₁, h₂]
  exact h₁ (h₂.comap _)

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