prodAssoc — Mathlib

English

The product of affine spaces is commutative up to affine isomorphism: P1 × P2 ≃ᵃ[k] P2 × P1.

Русский

Произведение аффинных пространств коммутативно до аффинного изоморфизма: P1 × P2 ≃ᵃ[k] P2 × P1.

LaTeX

$$$P_1 \times P_2 \cong^a_k P_2 \times P_1$$$

Lean4

/-- Product of affine spaces is associative up to affine isomorphism. -/
@[simps! apply symm_apply linear]
def prodAssoc : (P₁ × P₂) × P₃ ≃ᵃ[k] P₁ × (P₂ × P₃)
    where
  __ := Equiv.prodAssoc P₁ P₂ P₃
  linear := LinearEquiv.prodAssoc k V₁ V₂ V₃
  map_vadd' := by simp

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