English
The extension K over K⁺ is quadratic if K is CM; hence finrank(K over K⁺) = 2.
Русский
Расширение K над K⁺ квадратично, тогда размерности финальных степеней равны 2.
LaTeX
$$$\\operatorname{finrank}_{K^+}(K) = 2$.$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.NumberField.maximalRealSubfield]
public meta def
«_aux_Mathlib_NumberTheory_NumberField_CMField___delab_app__private_Mathlib_NumberTheory_NumberField_CMField_0_NumberField_IsCMField_termK⁺_1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 3
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.maximalRealSubfield))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
pure✝ >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(K⁺))
