Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.fintype.vector
! leanprover-community/mathlib commit 1126441d6bccf98c81214a0780c73d499f6721fe
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fintype.Pi
import Mathlib.Data.Sym.Basic

/-!
# `Vector α n` and `Sym α n` are fintypes when `α` is.
-/

variable {
α: Type ?u.215
α
:
Type _: Type (?u.5+1)
Type _
} instance
Vector.fintype: {α : Type u_1} → [inst : Fintype α] → {n : } → Fintype (Vector α n)
Vector.fintype
[
Fintype: Type ?u.8 → Type ?u.8
Fintype
α: Type ?u.5
α
] {
n:
n
:
: Type
} :
Fintype: Type ?u.13 → Type ?u.13
Fintype
(
Vector: Type ?u.14 → Type ?u.14
Vector
α: Type ?u.5
α
n:
n
) :=
Fintype.ofEquiv: {β : Type ?u.19} → (α : Type ?u.18) → [inst : Fintype α] → α βFintype β
Fintype.ofEquiv
_: Type ?u.18
_
(
Equiv.vectorEquivFin: (α : Type ?u.52) → (n : ) → Vector α n (Fin nα)
Equiv.vectorEquivFin
_: Type ?u.52
_
_:
_
).
symm: {α : Sort ?u.56} → {β : Sort ?u.55} → α ββ α
symm
#align vector.fintype
Vector.fintype: {α : Type u_1} → [inst : Fintype α] → {n : } → Fintype (Vector α n)
Vector.fintype
instance: {α : Type u_1} → [inst : DecidableEq α] → [inst : Fintype α] → {n : } → Fintype (Sym.Sym' α n)
instance
[
DecidableEq: Sort ?u.218 → Sort (max1?u.218)
DecidableEq
α: Type ?u.215
α
] [
Fintype: Type ?u.227 → Type ?u.227
Fintype
α: Type ?u.215
α
] {
n:
n
:
: Type
} :
Fintype: Type ?u.232 → Type ?u.232
Fintype
(
Sym.Sym': Type ?u.233 → Type ?u.233
Sym.Sym'
α: Type ?u.215
α
n:
n
) :=

Goals accomplished! 🐙
α: Type ?u.215

inst✝¹: DecidableEq α

inst✝: Fintype α

n:


α: Type ?u.215

inst✝¹: DecidableEq α

inst✝: Fintype α

n:


DecidableRel fun x x_1 => x x_1
α: Type ?u.215

inst✝¹: DecidableEq α

inst✝: Fintype α

n:


α: Type ?u.215

inst✝¹: DecidableEq α

inst✝: Fintype α

n:

x, y: Vector α n


Decidable ((fun x x_1 => x x_1) x y)
α: Type ?u.215

inst✝¹: DecidableEq α

inst✝: Fintype α

n:



Goals accomplished! 🐙
instance: {α : Type u_1} → [inst : DecidableEq α] → [inst : Fintype α] → {n : } → Fintype (Sym α n)
instance
[
DecidableEq: Sort ?u.508 → Sort (max1?u.508)
DecidableEq
α: Type ?u.505
α
] [
Fintype: Type ?u.517 → Type ?u.517
Fintype
α: Type ?u.505
α
] {
n:
n
:
: Type
} :
Fintype: Type ?u.522 → Type ?u.522
Fintype
(
Sym: Type ?u.523 → Type ?u.523
Sym
α: Type ?u.505
α
n:
n
) :=
Fintype.ofEquiv: {β : Type ?u.531} → (α : Type ?u.530) → [inst : Fintype α] → α βFintype β
Fintype.ofEquiv
_: Type ?u.530
_
Sym.symEquivSym': {α : Type ?u.566} → {n : } → Sym α n Sym.Sym' α n
Sym.symEquivSym'
.
symm: {α : Sort ?u.570} → {β : Sort ?u.569} → α ββ α
symm