∫ Утверждение Mathlib

_aux_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme_macroRulesprivate_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme_0_AlgebraicGeometry_termProj_1

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry._aux_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme___macroRules__private_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme_0_AlgebraicGeometry_termProj_1

← MathLib Explorer

English

A ∈ carrier f_deg q if and only if a certain homogeneous polynomial expression built from a and f lies in q.asIdeal.

Русский

A ∈ carrier f_deg q тогда и только тогда, когда соответствующее однородное выражение, построенное из a и f, лежит в q.asIdeal.

LaTeX

$$$a\in carrier f_{deg} \; q \Longleftrightarrow\; a\text{ формируется как полином, лежащий в }q.asIdeal$$$

Lean4

@[macro _private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.termProj]
public meta def
  _aux_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme___macroRules__private_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme_0_AlgebraicGeometry_termProj_1 :
    Macro✝ := fun
  | `(Proj) => `(«Proj».toLocallyRingedSpace 𝒜)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

Похожие утверждения