coe_prodCongr — Mathlib

English

As above, the affine map underlying prodCongr equals the product of the underlying maps.

Русский

Как выше, базовая аффинная карта, лежащая в основе prodCongr, равна произведению базовых карт.

LaTeX

$$$\bigl(e_1.prodCongr e_2\bigr) = (e_1) \text{.prodMap} (e_2)$$$

Lean4

@[simp, norm_cast]
theorem coe_prodCongr : (e₁.prodCongr e₂ : P₁ × P₃ →ᵃ[k] P₂ × P₄) = (e₁ : P₁ →ᵃ[k] P₂).prodMap (e₂ : P₃ →ᵃ[k] P₄) :=
  rfl

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