Commit 2024-10-16 04:43 e11ad74a

View on Github →

chore: split Data.Finite.Basic (#17796)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/FintypeCat.lean

Modified Mathlib/CategoryTheory/Galois/Decomposition.lean

Modified Mathlib/CategoryTheory/Limits/FintypeCat.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

Modified Mathlib/Data/Fin/Tuple/BubbleSortInduction.lean

Modified Mathlib/Data/Fin/Tuple/Sort.lean

Modified Mathlib/Data/Finite/Basic.lean

deleted theorem Finite.prod_left

deleted theorem Finite.prod_right

deleted theorem Finite.sum_left

deleted theorem Finite.sum_right

Created Mathlib/Data/Finite/Powerset.lean

Created Mathlib/Data/Finite/Prod.lean

added theorem Finite.prod_left

added theorem Finite.prod_right

Created Mathlib/Data/Finite/Sigma.lean

Created Mathlib/Data/Finite/Sum.lean

added theorem Finite.sum_left

added theorem Finite.sum_right

Created Mathlib/Data/Finite/Vector.lean

Modified Mathlib/Data/Finset/Preimage.lean

Modified Mathlib/Data/FunLike/Fintype.lean

Modified Mathlib/Data/Set/Finite.lean

modified theorem List.finite_length_eq

Modified Mathlib/GroupTheory/Abelianization.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/GroupTheory/SpecificGroups/Dihedral.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/ModelTheory/DirectLimit.lean