coprod_inl_inr

Mathlib.Topology.Algebra.Module.LinearMapPiProd

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coprod_inl_inr

English

The coprod of the injections inl and inr is the identity on the product M × N.

Русский

Копрод вложений inl и inr равенства идентичности на произведении M × N.

LaTeX

$$$$ \text{coprod} (\mathrm{inl}\, , \mathrm{inr}) = \mathrm{id}_{M \times N} $$$$

Lean4

@[simp]
theorem coprod_inl_inr : ContinuousLinearMap.coprod (.inl R M N) (.inr R M N) = .id R (M × N) :=
  coe_injective <| LinearMap.coprod_inl_inr

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

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

Разделы

Аффилиация

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