prod — Mathlib

English

If Q1 ≃ Q1' and Q2 ≃ Q2' then (Q1.prod Q2) ≃ (Q1'.prod Q2').

Русский

Если Q1 эквивалентна Q1', и Q2 эквивалентна Q2', то их произведение эквивалентно произведению их эквивалентов.

LaTeX

$$If e1: Q1.Equivalent Q1' and e2: Q2.Equivalent Q2' then (Q1.prod Q2).Equivalent (Q1'.prod Q2')$$

Lean4

theorem prod {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {Q₁' : QuadraticMap R N₁ P}
    {Q₂' : QuadraticMap R N₂ P} (e₁ : Q₁.Equivalent Q₁') (e₂ : Q₂.Equivalent Q₂') :
    (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂') :=
  Nonempty.map2 IsometryEquiv.prod e₁ e₂

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