finTwoArrow — Mathlib

English

There is a linear equivalence between vectors in M² = Fin 2 → M and M × M.

Русский

Существует линейное эквивалентство между векторами в M² = Fin 2 → M и M × M.

LaTeX

$$$$ (Fin 2 \\to M) \\simeq_{\\!R} M \\times M, $$$$

Lean4

/-- Linear equivalence between vectors in `M² = Fin 2 → M` and `M × M`. -/
@[simps! -fullyApplied]
def finTwoArrow : (Fin 2 → M) ≃ₗ[R] M × M :=
  { finTwoArrowEquiv M, piFinTwo R fun _ => M with }

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