ofCMExtension — Mathlib

English

If K/F is a CM-extension, then K is a CM-field.

Русский

Если K/F является CM-расширением, то K — это CM-поле.

LaTeX

$$$\\text{If } K/F \\text{ is CM-extension, then } K \\text{ is CM-field.}$$$

Lean4

/-- If `K/F` is a CM-extension then `K` is a CM-field.
-/
theorem _root_.NumberField.IsCMField.ofCMExtension : IsCMField K where
  is_quadratic :=
    ⟨(IsQuadraticExtension.finrank_eq_two F K) ▸
        finrank_eq_of_equiv_equiv (CMExtension.equivMaximalRealSubfield F K).symm (RingEquiv.refl K) (by ext; simp)⟩

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