# Documentation

Mathlib.Data.Fintype.Quotient

# Quotients of families indexed by a finite type #

This file provides Quotient.finChoice, a mechanism to go from a finite family of quotients to a quotient of finite families.

## Main definitions #

• Quotient.finChoice
def Quotient.finChoiceAux {ι : Type u_1} [] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (l : List ι) :
((i : ι) → i lQuotient (S i)) → Quotient inferInstance

An auxiliary function for Quotient.finChoice. Given a collection of setoids indexed by a type ι, a (finite) list l of indices, and a function that for each i ∈ l gives a term of the corresponding quotient type, then there is a corresponding term in the quotient of the product of the setoids indexed by l.

Equations
• One or more equations did not get rendered due to their size.
• = Quotient.mk inferInstance fun i h => nomatch (_ : False)
Instances For
theorem Quotient.finChoiceAux_eq {ι : Type u_1} [] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (l : List ι) (f : (i : ι) → i lα i) :
(Quotient.finChoiceAux l fun i h => Quotient.mk (S i) (f i h)) = Quotient.mk inferInstance f
def Quotient.finChoice {ι : Type u_1} [] [] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (f : (i : ι) → Quotient (S i)) :
Quotient inferInstance

Given a collection of setoids indexed by a fintype ι and a function that for each i : ι gives a term of the corresponding quotient type, then there is corresponding term in the quotient of the product of the setoids.

Instances For
theorem Quotient.finChoice_eq {ι : Type u_1} [] [] {α : ιType u_2} [(i : ι) → Setoid (α i)] (f : (i : ι) → α i) :
(Quotient.finChoice fun i => Quotient.mk (inst✝ i) (f i)) = Quotient.mk inferInstance f