one_gradedMul — Mathlib

English

The graded multiplication sends the unit to the unit, i.e., gradedMul(1, x) = x.

Русский

Градуированное умножение отправляет единицу в единицу: gradedMul(1, x) = x.

LaTeX

$$$$ gradedMul_R(1, x) = x. $$$$

Lean4

theorem one_gradedMul (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) : gradedMul R 𝒜 ℬ 1 x = x := by
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specialize `map_one` to avoid timeouts.
  simpa only [RingHom.map_one, one_smul] using algebraMap_gradedMul 𝒜 ℬ 1 x

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