Commit 2024-07-30 08:44 c1478df3

View on Github →

chore(DirectSum): drop DecidableEq assumption (#15287)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

modified theorem DirectSum.coeAddMonoidHom_eq_dfinsupp_sum

modified theorem DirectSum.finite_support

modified theorem DirectSum.support_subset