mathlib

25e36bea - chore(data/fintype/basic): `fintype α/β` from `fintype α ⊕ β` (#7736)

chore(data/fintype/basic): `fintype α/β` from `fintype α ⊕ β` (#7736) Also renaming the equivalent `α × β` versions, for consistency. Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>