prodCongr_apply — Mathlib

English

The action of the product-congruence on a pair is componentwise: (e.prodCongr e') (x,y) = (e x, e' y).

Русский

Действие произведения-конгруэнции на пару есть по компонентам: (e.prodCongr e')(x,y) = (e x, e' y).

LaTeX

$$$$ (e \prodCongr e')(x,y) = (e x, e' y). $$$$

Lean4

@[simp, norm_cast]
theorem prodCongr_apply [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) (x) :
    e.prodCongr e' x = (e x.1, e' x.2) :=
  rfl

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