English
Relates z.num.1 ∈ carrier f_deg q with HomogeneousLocalization.mk z ∈ q.asIdeal.
Русский
Связь z.num.1 ∈ carrier f_deg q с HomogeneousLocalization.mk z ∈ q.asIdeal.
LaTeX
$$$z.num.1 \in carrier f_deg q \iff HomogeneousLocalization.mk z \in q.asIdeal$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.AlgebraicGeometry.Spec.locallyRingedSpaceObj]
public meta def
_aux_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme___delab_app__private_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme_0_AlgebraicGeometry_termSpec__1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 1
(getExpr✝ >>= fun e✝ =>
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.Spec.locallyRingedSpaceObj))
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `CommRingCat.of)) (matchVar✝ `ring)) pure✝) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => MatchState.delabVar✝ s✝ `ring (some✝ e✝) >>= fun ring => withHeadRefIfTagAppFns✝ `(Spec $ring))
