Skip to content

Commit 98746ef

Browse files
LukasMiasChrisHughes24
LukasMias
and
ChrisHughes24
committed
feat: port Algebra.BigOperators.Finprod (#1766)
Some mathport warnings in here that I left in for the experts to review. Rest should be done! Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
1 parent 2b625ad commit 98746ef

File tree

2 files changed

+1333
-0
lines changed

2 files changed

+1333
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import Mathlib.Algebra.Abs
22
import Mathlib.Algebra.Associated
33
import Mathlib.Algebra.BigOperators.Basic
4+
import Mathlib.Algebra.BigOperators.Finprod
45
import Mathlib.Algebra.BigOperators.Multiset.Basic
56
import Mathlib.Algebra.BigOperators.Multiset.Lemmas
67
import Mathlib.Algebra.BigOperators.NatAntidiagonal

0 commit comments

Comments
 (0)