Commit 2023-01-19 16:43 9c7b0eba

View on Github →

feat: port Data.Fintype.Option (#1677)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Option.lean

added theorem Finite.induction_empty_option

added theorem Fintype.card_option

added theorem Fintype.induction_empty_option

added def Fintype.truncRecEmptyOption

added def fintypeOfOption

added def fintypeOfOptionEquiv

added theorem univ_option