Commit 2023-05-24 10:36 3d4bf22a

View on Github →

feat: port Data.Fintype.Quotient (#3971)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Quotient.lean

added def Quotient.finChoice

added def Quotient.finChoiceAux

added theorem Quotient.finChoiceAux_eq

added theorem Quotient.finChoice_eq