equivOfIsometry_trans — Mathlib

English

If e1: Q1 →qᵢ Q2 and e2: Q2 →qᵢ Q3 are isometry equivalences, then the corresponding Clifford algebra equivalences satisfy: equivOfIsometry e1 trans equivOfIsometry e2 = equivOfIsometry (e1.trans e2).

Русский

Если e1: Q1 →qᵢ Q2 и e2: Q2 →qᵢ Q3 — эквивалентные изометрии, то соответствующие эквиваленты CliffordAlgebra удовлетворяют: equivOfIsometry e1.trans e2 = equivOfIsometry (e1.trans e2).

LaTeX

$$$ (\mathrm{equivOfIsometry} e_1).\mathrm{trans} (\mathrm{equivOfIsometry} e_2) = \mathrm{equivOfIsometry} (e_1.\mathrm{trans} e_2). $$$

Lean4

@[simp]
theorem equivOfIsometry_trans (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q₂.IsometryEquiv Q₃) :
    (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃) :=
  by
  ext x
  exact AlgHom.congr_fun (map_comp_map _ _) x

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