Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-30 23:39 94825b2b

View on Github →

chore(algebra/module/basic): remove dependency on finiteness (#17764)

Estimated changes

Modified src/algebra/module/basic.lean

deleted theorem finset.cast_card

deleted theorem finset.sum_smul

deleted theorem list.sum_smul

deleted theorem multiset.sum_smul

Created src/algebra/module/big_operators.lean

added theorem finset.cast_card

added theorem finset.sum_smul

added theorem list.sum_smul

added theorem multiset.sum_smul

Modified src/algebra/module/torsion.lean

Modified src/algebra/monoid_algebra/basic.lean

Modified src/algebra/order/rearrangement.lean

Modified src/algebra/support.lean

Modified src/combinatorics/pigeonhole.lean

Modified src/linear_algebra/affine_space/combination.lean

Modified src/linear_algebra/dimension.lean

Modified src/number_theory/arithmetic_function.lean

Modified src/ring_theory/algebra_tower.lean