prodCongr — Mathlib

English

Applying a product congruence to a pair yields componentwise application: e1.prodCongr e2 (p1,p3) = (e1 p1, e2 p3).

Русский

Действуя на пару через произведение конгруэнции, получаем применение по компонентам: e1.prodCongr e2 (p1,p3) = (e1 p1, e2 p3).

LaTeX

$$$e_1.prodCongr e_2\,(p_1,p_3) = (e_1(p_1), e_2(p_3))$$$

Lean4

/-- Product of two affine equivalences. The map comes from `Equiv.prodCongr` -/
@[simps linear]
def prodCongr : P₁ × P₃ ≃ᵃ[k] P₂ × P₄ where
  __ := Equiv.prodCongr e₁ e₂
  linear := e₁.linear.prodCongr e₂.linear
  map_vadd' := by simp

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