Commit 2022-04-22 06:47 9db59165
View on Github →fix(data/fintype/basic): fix fintype_of_option_equiv (#13466)
A type is a fintype if its successor (using option) is a fintype
This fixes an error introduced in #13086.
fix(data/fintype/basic): fix fintype_of_option_equiv (#13466)
A type is a fintype if its successor (using option) is a fintype
This fixes an error introduced in #13086.