Commit 2023-05-22 03:13 78f62c89

View on Github →

chore: forward-port leanprover-community/mathlib#19050 (#4119)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

Modified Mathlib/Data/Finset/Pi.lean

added theorem Finset.Pi.cons_injective

deleted theorem Finset.pi_cons_injective

Modified Mathlib/Data/Multiset/Pi.lean

added theorem Multiset.Pi.cons_injective

added theorem Multiset.pi.cons_eta

deleted theorem Multiset.pi.cons_ext

deleted theorem Multiset.pi_cons_injective