Commit 2024-03-16 21:39 de6d9520

View on Github →

chore(Preadditive/Biproducts): fix Decidable/Fintype (#11422)

Assume [Finite J] instead of [Fintype J] whenever we don't need data to formulate the theorem.
Drop [DecidableEq] assumptions in biproduct.reindex.

Estimated changes

Modified Mathlib/CategoryTheory/Preadditive/Biproducts.lean

modified theorem CategoryTheory.Limits.HasBiproduct.of_hasCoproduct

modified theorem CategoryTheory.Limits.HasBiproduct.of_hasProduct

modified theorem CategoryTheory.Limits.biproduct.lift_matrix

modified theorem CategoryTheory.Limits.biproduct.map_matrix

modified theorem CategoryTheory.Limits.biproduct.matrix_desc

modified theorem CategoryTheory.Limits.biproduct.matrix_map

modified def CategoryTheory.Limits.biproduct.reindex