Commit 2024-02-13 04:00 f236307f

View on Github →

chore(LinearAlgebra/Finsupp): Fintype -> Finite (#10463)

Estimated changes

Modified Mathlib/LinearAlgebra/Finsupp.lean

modified theorem LinearMap.leftInverse_splittingOfFunOnFintypeSurjective

modified def LinearMap.splittingOfFunOnFintypeSurjective

modified theorem LinearMap.splittingOfFunOnFintypeSurjective_injective

modified theorem LinearMap.splittingOfFunOnFintypeSurjective_splits