coe_prodCongr

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#LinearEquiv.coe_prodCongr

English

Reiterates that the underlying AddEquiv of prodCongr matches the canonical AddEquiv.

Русский

Повторение того, что база AddEquiv сочетается с prodCongr.

LaTeX

$$$(AddEquiv).toAddEquiv (LinearEquiv.prodCongr) = AddEquiv.prodCongr M M_2 M_3 M_4$$$

Lean4

@[simp, norm_cast]
theorem coe_prodCongr : (e₁.prodCongr e₂ : M × M₃ →ₗ[R] M₂ × M₄) = (e₁ : M →ₗ[R] M₂).prodMap (e₂ : M₃ →ₗ[R] M₄) :=
  rfl

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

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

Разделы

Аффилиация

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