Commit 2025-02-14 19:33 29f215ff

View on Github →

feat: missing lemmas for homogeneous algebras of finite type (#21795)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

added theorem Finset.prod_attach_eq_prod_dite

Modified Mathlib/Algebra/DirectSum/Internal.lean

added theorem DirectSum.coe_mul_of_apply_of_mem_zero

added theorem DirectSum.coe_of_mul_apply_of_mem_zero

added theorem SetLike.GradeZero.algebraMap_apply

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

added theorem Localization.mk_prod

Modified Mathlib/RingTheory/GradedAlgebra/Basic.lean

added theorem DirectSum.coe_decompose_mul_of_left_mem_zero

added theorem DirectSum.coe_decompose_mul_of_right_mem_zero