English
There exists a finite type embedding from a polynomial algebra in s variables into R with integral extension.
Русский
Пусть существует вложение из многочленовой алгебры в R, интегрально расширяющееся.
LaTeX
$$∃ s, ∃ g: (MvPolynomial (Fin s) k) →ₐ[k] R, Function.Injective g ∧ g.IsIntegral$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ lam]
public meta def
_aux_Mathlib_RingTheory_NoetherNormalization___delab_app__private_Mathlib_RingTheory_NoetherNormalization_0_NoetherNormalization_termR_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
getExpr✝ >>= fun e✝ =>
(matchLambda✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fin))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HAdd.hAdd))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
pure✝)
(matchFVar✝ `n (matchExpr✝ (Expr.isConstOf✝ · `Nat))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat)) (matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 1))
pure✝)))
(fun n✝ =>
matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `HPow.hPow))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
pure✝¹)
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `HAdd.hAdd))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
pure✝¹)
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `OfNat.ofNat))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(natLitMatcher✝¹ 2))
pure✝¹))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `MvPolynomial.totalDegree))
(matchFVar✝¹ `k (matchExpr✝¹ isType'✝)))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Fin))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `HAdd.hAdd))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
pure✝¹)
(matchFVar✝¹ `n (matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat))))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `OfNat.ofNat))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(natLitMatcher✝¹ 1))
pure✝¹))))
pure✝¹)
(matchFVar✝¹ `f
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `MvPolynomial))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Fin))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `HAdd.hAdd))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
pure✝¹)
(matchFVar✝¹ `n (matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat))))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `OfNat.ofNat))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(natLitMatcher✝¹ 1))
pure✝¹))))
(matchFVar✝¹ `k (matchExpr✝¹ isType'✝)))
pure✝¹)))))
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Fin.val))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `HAdd.hAdd))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
pure✝¹)
(matchFVar✝¹ `n (matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat))))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `OfNat.ofNat))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `Nat)))
(natLitMatcher✝¹ 1))
pure✝¹)))
(matchExpr✝¹ (· == n✝)))) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(r)
