English
A criterion equivalence between membership of a in carrier and membership of a constructed homogeneous localization element in q.asIdeal.
Русский
Критерий эквивалентности принадлежности a carrier и принадлежности сконструированного однородного локализованного элемента q.asIdeal.
LaTeX
$$$a\in carrier f_deg q \iff (HomogeneousLocalization.mk(...)) \in q.asIdeal$$$
Lean4
@[macro _private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.«termProj.T»]
public meta def
«_aux_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme___macroRules__private_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme_0_AlgebraicGeometry_termProj.T_1» :
Macro✝ := fun
| `(Proj.T) =>
`(PresheafedSpace.carrier <|
SheafedSpace.toPresheafedSpace <| LocallyRingedSpace.toSheafedSpace <| «Proj».toLocallyRingedSpace 𝒜)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
