decompose_symm_one

Mathlib.RingTheory.GradedAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#DirectSum.decompose_symm_one

English

The inverse of the decomposition sends 1 to 1.

Русский

Обратная декомпозиция отправляет 1 в 1.

LaTeX

$$$ (\mathrm{decompose} 𝒜)^{-1}(1) = 1. $$$

Lean4

@[simp]
theorem decompose_symm_one : (decompose 𝒜).symm 1 = (1 : A) :=
  map_one (decomposeRingEquiv 𝒜).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru