isSetoid — Mathlib

English

The setoid on Vector α n is the lift of List.Perm: two vectors are equivalent if their underlying lists are permutation-equivalent.

Русский

На векторе Vector α n задана эквивалентность по Perm из List, т. е. два вектора эквивалентны, если их списочные представления приводимы перестановкой.

LaTeX

$$$\\text{isSetoid}(\\alpha,n) = (\\text{List}.\\text{isSetoid}(\\alpha)).\\text{comap} (\\text{Subtype}.\\text{val})$$$

Lean4

/-- This is the `List.Perm` setoid lifted to `Vector`.

See note [reducible non-instances].
-/
abbrev isSetoid (α : Type*) (n : ℕ) : Setoid (Vector α n) :=
  (List.isSetoid α).comap Subtype.val

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