English
T1 is a noncomputable algebra hom defined by aeval with X0 fixed and Xi adjusted by c·X0^ri for i > 0.
Русский
T1 — определение алгебраического гомоморфа через выражение на X_i.
LaTeX
$$NoetherNormalization.T1$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.HAdd.hAdd]
public meta def
_aux_Mathlib_RingTheory_NoetherNormalization___delab_app__private_Mathlib_RingTheory_NoetherNormalization_0_NoetherNormalization_termUp_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 6
(getExpr✝ >>= fun e✝ =>
(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✝))) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(up))
