English
If D is a noncommutative division ring algebraic over its center k, there exists x not in k that is separable over k.
Русский
Если D некоммутативное деление кольца, алгебраично над своим центром k, существует x не в k, сепарабельный над k.
LaTeX
$$$\\exists x\\notin k,\\ IsSeparable\\ k\\ x$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Subring.center]
public meta def
_aux_Mathlib_FieldTheory_JacobsonNoether___delab_app__private_Mathlib_FieldTheory_JacobsonNoether_0_JacobsonNoether_termK_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 2
(getExpr✝ >>= fun e✝ =>
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Subring.center)) (matchFVar✝ `D (matchExpr✝ isType'✝)))
pure✝ >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(k))
