Commit 2025-02-17 17:27 9d1a5226
View on Github →chore(Data/Fintype): split Data/Fintype/Basic.lean
(#21831)
This PR splits Data.Fintype.Basic
into the following files:
Data.Fintype.Defs
: definition ofFintype
andFinset.univ
Data.Finset.BooleanAlgebra
: showsFinset
is a boolean algebra (withFinset.univ
as top element)Data.Fintype.Basic
: instances forFintype
on most basic types such as products and pi typesData.Fintype.Group
: finiteness and additive/multiplicative structuresData.Fintype.Inv
: computably choosing existential witnesses and constructing inverse functionsData.Fintype.OfMap
: constructors forFintype
given maps from/to finite typesData.Fintype.Sets
: equivalence betweenSet
andFinset
on finite types A particular goal is to avoid importing the algebra hierarchy while working on finiteness and eventually into measure theory.