Commit 2021-05-30 09:54 25e36bea
View on Github →chore(data/fintype/basic): fintype α/β from fintype α ⊕ β (#7736)
Also renaming the equivalent α × β versions, for consistency.
chore(data/fintype/basic): fintype α/β from fintype α ⊕ β (#7736)
Also renaming the equivalent α × β versions, for consistency.