equivVector — Mathlib

English

There is a canonical bijection between vectorsProdEqOne G n and List.Vector G (n-1).

Русский

Существует каноническое биекция между vectorsProdEqOne G n и List.Vector G (n-1).

LaTeX

$$equivVector : ∀ n, vectorsProdEqOne G n).Elem ≃ List.Vector G (n-1)$$

Lean4

/-- Given a vector `v` of length `n` whose product is 1, make a vector of length `n - 1`,
by deleting the last entry of `v`. -/
def equivVector : ∀ n, vectorsProdEqOne G n ≃ List.Vector G (n - 1)
  | 0 => (ofUnique (vectorsProdEqOne G 0) (vectorsProdEqOne G 1)).trans (vectorEquiv G 0).symm
  | (n + 1) => (vectorEquiv G n).symm

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