Theorem Fintype.prod_of_injective

Modification history

2025-04-19 14:06
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
chore(Algebra/BigOperators/Group/Finset/Basic): use meaningful letter names (#24123) …
Modified Fintype.prod_of_injectiveView on Github →
2025-04-10 03:41
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
chore: split `Algebra.BigOperators.Group.Finset.Basic` (#23897) …
Modified Fintype.prod_of_injectiveView on Github →
2024-03-22 13:23
Mathlib/Algebra/BigOperators/Basic.lean
chore(Algebra/BigOperators/Basic): argument name (#11571)
Modified Fintype.prod_of_injectiveView on Github →
2024-01-06 14:22
Mathlib/Algebra/BigOperators/Basic.lean
feat: Finite sum under an injective map (#9226) …
Added Fintype.prod_of_injectiveView on Github →