projZeroRingHom'_surjective — Mathlib

English

The surjectivity of the zeroth projection map is maintained under the restriction to homogeneous components.

Русский

Сюрьективность нулевой проекции сохраняется при ограничении к однородным компонентам.

LaTeX

$$Same as 176731/176732 surjectivity assertion for 𝒜.$$

Lean4

/-- The ring homomorphism `GradedRing.projZeroRingHom' 𝒜` is surjective. -/
theorem projZeroRingHom'_surjective : Function.Surjective (GradedRing.projZeroRingHom' 𝒜) :=
  Function.RightInverse.surjective (GradedRing.projZeroRingHom'_apply_coe 𝒜)

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