domDomCongr_refl

Mathlib.LinearAlgebra.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#AlternatingMap.domDomCongr_refl

English

Composition of domDomCongr along two arrows equals the domDomCongr along the composition of arrows.

Русский

Сложение domDomCongr вдоль двух стрелок равно domDomCongr вдоль композиции стрелок.

LaTeX

$$(domLCongr σ1) .trans (domLCongr σ2) = domLCongr (σ1.trans σ2)$$

Lean4

@[simp]
theorem domDomCongr_refl (f : M [⋀^ι]→ₗ[R] N) : f.domDomCongr (Equiv.refl ι) = f :=
  rfl

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

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

Разделы

Аффилиация

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