Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Yury Kudryashov, Yaël Dillies
! This file was ported from Lean 3 source module algebra.module.big_operators
! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Module.Basic
import Mathlib.GroupTheory.GroupAction.BigOperators
/-!
# Finite sums over modules over a ring
-/
open BigOperators
variable { α β R M ι : Type _ : Type (?u.38169+1)}
section AddCommMonoid
variable [ Semiring R ] [ AddCommMonoid : Type ?u.10850 → Type ?u.10850 M ] [ Module R M ] ( r s : R ) ( x y : M )
theorem List.sum_smul { l : List R } { x : M } : l . sum • x = ( l . map fun r ↦ r • x ). sum :=
(( smulAddHom R M ). flip x ). map_list_sum l
#align list.sum_smul List.sum_smul
theorem Multiset.sum_smul { l : Multiset R } { x : M } : l . sum • x = ( l . map fun r ↦ r • x ). sum :=
(( smulAddHom R M ). flip x ). map_multiset_sum l
#align multiset.sum_smul Multiset.sum_smul
theorem Multiset.sum_smul_sum { s : Multiset R } { t : Multiset M } :
s . sum • t . sum = (( s ×ˢ t ). map fun p : R × M ↦ p . fst : {α : Type ?u.21742} → {β : Type ?u.21741} → α × β α • p . snd : {α : Type ?u.21748} → {β : Type ?u.21747} → α × β β ). sum := by
induction' s using Multiset.induction with a s ih
· simp
· simp [ add_smul , ih , ← Multiset.smul_sum ]
#align multiset.sum_smul_sum Multiset.sum_smul_sum
theorem Finset.sum_smul { f : ι → R } { s : Finset ι } { x : M } :
(∑ i in s , f i ) • x = ∑ i in s , f i • x := (( smulAddHom R M ). flip x ). map_sum f s
#align finset.sum_smul Finset.sum_smul
theorem Finset.sum_smul_sum { f : α → R } { g : β → M } { s : Finset α } { t : Finset β } :
((∑ i in s , f i ) • ∑ i in t , g i ) = ∑ p in s ×ˢ t , f p . fst : {α : Type ?u.36929} → {β : Type ?u.36928} → α × β α • g p . snd : {α : Type ?u.36935} → {β : Type ?u.36934} → α × β β := by
(∑ i in s , f i ) • ∑ i in t , g i = ∑ p in s ×ˢ t f p .fst• g p .snd rw [ (∑ i in s , f i ) • ∑ i in t , g i = ∑ p in s ×ˢ t f p .fst• g p .snd Finset.sum_product , (∑ i in s , f i ) • ∑ i in t , g i = ∑ x in s , ∑ y in t , f (x , y ) .fst• g (x , y ) .snd (∑ i in s , f i ) • ∑ i in t , g i = ∑ p in s ×ˢ t f p .fst• g p .snd Finset.sum_smul , ∑ i in s , f i • ∑ i in t , g i = ∑ x in s , ∑ y in t , f (x , y ) .fst• g (x , y ) .snd (∑ i in s , f i ) • ∑ i in t , g i = ∑ p in s ×ˢ t f p .fst• g p .snd Finset.sum_congr rfl : ∀ {α : Sort ?u.37874} {a : α }, a = a Finset.sum s ?m.37872 = ∑ x in s , ∑ y in t , f (x , y ) .fst• g (x , y ) .snd ∀ (x : α ), x ∈ s f x • ∑ i in t , g i = ?m.37872 x α → M
] ∀ (x : α ), x ∈ s f x • ∑ i in t , g i = ∑ y in t , f (x , y ) .fst• g (x , y ) .snd
(∑ i in s , f i ) • ∑ i in t , g i = ∑ p in s ×ˢ t f p .fst• g p .snd intros f x✝ • ∑ i in t , g i = ∑ y in t , f (x✝ , y ) .fst• g (x✝ , y ) .snd
(∑ i in s , f i ) • ∑ i in t , g i = ∑ p in s ×ˢ t f p .fst• g p .snd rw [ f x✝ • ∑ i in t , g i = ∑ y in t , f (x✝ , y ) .fst• g (x✝ , y ) .snd Finset.smul_sum ∑ x in t , f x✝ • g x = ∑ y in t , f (x✝ , y ) .fst• g (x✝ , y ) .snd ]
#align finset.sum_smul_sum Finset.sum_smul_sum
end AddCommMonoid
theorem Finset.cast_card [ CommSemiring : Type ?u.38178 → Type ?u.38178 R ] ( s : Finset α ) : ( s . card : R ) = ∑ a in s , 1 := by
rw [ Finset.sum_const , Nat.smul_one_eq_coe : ∀ {R : Type ?u.39255} [inst : Semiring R m : ℕ ), m • 1 = ↑m ]
#align finset.cast_card Finset.cast_card