decompose'_eq

Mathlib.Algebra.DirectSum.Decomposition

URI: https://scilib.ai/kg/mathlib#DirectSum.Decomposition.decompose'_eq

English

The auxiliary decomposition field decompose' coincides with the primary decomposition decompose.

Русский

Вспомогательное поле декомпозиции decompose' совпадает с основной декомпозиции decompose.

LaTeX

$$$\mathrm{Decomposition}.decompose' = \mathrm{decompose}_{\mathcal{M}}$$$

Lean4

@[simp]
theorem decompose'_eq : Decomposition.decompose' = decompose ℳ :=
  rfl

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

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

Разделы

Аффилиация

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