projZeroRingHom'_apply_coe — Mathlib

English

The coerced projection to zero equals the standard projection to zero.

Русский

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

LaTeX

$$$\big(\mathrm{projZeroRingHom}' 𝒜\, a\big) = \mathrm{projZeroRingHom} 𝒜 a$ for all a.$$

Lean4

@[simp]
theorem projZeroRingHom'_apply_coe (a : 𝒜 0) : GradedRing.projZeroRingHom' 𝒜 a = a := by ext;
  simp only [coe_projZeroRingHom'_apply, projZeroRingHom_apply, decompose_coe, of_eq_same]

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