Commit 2024-05-26 11:13 20863d98

View on Github →

feat(Mathlib/Data/Fintype/Quotient): Trunc version of Quotient.finChoice (#13025)

Estimated changes

added def Trunc.finChoice
added theorem Trunc.finChoice_eq