English
The symmetry of prodAssoc equals the standard product symmetry, i.e., the order of pairing in a triple product can be rearranged without changing the underlying mapping.
Русский
Симметрия prodAssoc равна стандартной симметрии произведения; порядок склейки в троичном произведении можно поменять без изменения отображения.
LaTeX
$$coe_prodAssoc_symm : ((prodAssoc R E E₂ E₃).symm) = (Equiv.prodAssoc E E₂ E₃).symm$$
Lean4
/-- The natural equivalence `(E × E₂) × E₃ ≃ E × (E₂ × E₃)` is a linear isometry. -/
def prodAssoc [Module R E₂] [Module R E₃] : (E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃ :=
{ LinearEquiv.prodAssoc R E E₂ E₃ with
norm_map' := by
rintro ⟨⟨e, f⟩, g⟩
simp only [LinearEquiv.prodAssoc_apply, AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
AddEquiv.coe_prodAssoc, Equiv.prodAssoc_apply, Prod.norm_def, max_assoc] }
