coe_prodCongr — Mathlib

English

The product-congruence map coincides with the product of the component linear maps at the level of continuous linear maps.

Русский

Обе карты совпадают с произведением компонентных линейных отображений на уровне непрерывных линейных отображений.

LaTeX

$$$$ (e.prodCongr e').toLinearMap = e.toLinearMap.prodMap e'.toLinearMap. $$$$

Lean4

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

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