Def Quotient.finChoiceAux
Modification history
2024-11-04 10:42
Mathlib/Data/Fintype/Quotient.lean
feat: quotient lift on a finite family (#5576) …
Deleted Quotient.finChoiceAuxView on Github →2023-08-10 19:52
Mathlib/Data/Fintype/Quotient.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified Quotient.finChoiceAuxView on Github →2023-05-24 10:36
Mathlib/Data/Fintype/Quotient.lean
feat: port Data.Fintype.Quotient (#3971)
Added Quotient.finChoiceAuxView on Github →