English
If a ∈ 𝒜(nm) and m>0, then a ∈ carrier f_deg q iff the corresponding HomogeneousLocalization element lies in q.asIdeal.
Русский
Если a ∈ 𝒜(nm) и m>0, тогда a ∈ carrier f_deg q тогда и только тогда, когда соответствующий элемент HomogeneousLocalization лежит в q.asIdeal.
LaTeX
$$$a\in 𝒜(nm) \Rightarrow (a\in carrier f_deg q) \Leftrightarrow (HomogeneousLocalization.mk(...) ) \in q.asIdeal$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.AlgebraicGeometry.Proj.toLocallyRingedSpace]
public meta def
_aux_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme___delab_app__private_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme_0_AlgebraicGeometry_termProj_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 7
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.Proj.toLocallyRingedSpace))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
(matchFVar✝ `A (matchExpr✝ isType'✝)))
pure✝)
pure✝)
pure✝)
(matchFVar✝ `𝒜
(matchForall✝ (matchExpr✝ (Expr.isConstOf✝ · `Nat))
(fun n✝ =>
matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Submodule))
(matchFVar✝¹ `R (matchExpr✝¹ isType'✝¹)))
(matchFVar✝¹ `A (matchExpr✝¹ isType'✝¹)))
pure✝¹)
pure✝¹)
pure✝¹))))
pure✝ >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(Proj))
