Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-03 13:15 6f6739f8

View on Github →

chore(algebra/star/basic): split out big_operators import (#17792) cf https://github.com/leanprover-community/mathlib/pull/17772#issuecomment-1334662059, cc @eric-wieser

Estimated changes

Modified archive/100-theorems-list/42_inverse_triangle_sum.lean

Modified src/algebra/star/basic.lean

deleted theorem star_prod

deleted theorem star_sum

Created src/algebra/star/big_operators.lean

added theorem star_prod

added theorem star_sum

Modified src/data/matrix/basic.lean