projZeroRingHom' — Mathlib

English

Applying the zero-degree projection to an element of 𝒜0 returns the element itself.

Русский

Применение проекции нулевой степени к элементу 𝒜0 возвращает сам элемент.

LaTeX

$$$\mathrm{projZeroRingHom}' 𝒜 \; (a) = a \quad \text{for } a \in 𝒜(0).$$$

Lean4

/-- The ring homomorphism from `A` to `𝒜 0` sending every `a : A` to `a₀`. -/
def projZeroRingHom' : A →+* 𝒜 0 :=
  ((GradedRing.projZeroRingHom 𝒜).codRestrict _ fun _x => SetLike.coe_mem _ : A →+* SetLike.GradeZero.subsemiring 𝒜)

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