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 Cmdinstead of Ctrl.
/-
Copyright (c) 2019 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro

! This file was ported from Lean 3 source module data.rat.big_operators
! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Rat.Cast
import Mathlib.Algebra.BigOperators.Basic

/-! # Casting lemmas for rational numbers involving sums and products
-/

open BigOperators

variable {
ι: Type ?u.2119
ι
α: Type ?u.89
α
:
Type _: Type (?u.5+1)
Type _
} namespace Rat section WithDivRing variable [
DivisionRing: Type ?u.2125 → Type ?u.2125
DivisionRing
α: Type ?u.89
α
] [
CharZero: (R : Type ?u.1124) → [inst : AddMonoidWithOne R] → Prop
CharZero
α: Type ?u.11
α
] @[simp, norm_cast] theorem
cast_list_sum: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : List ℚ), ↑(List.sum s) = List.sum (List.map Rat.cast s)
cast_list_sum
(s :
List: Type ?u.164 → Type ?u.164
List
ℚ: Type
ℚ
) : (↑s.
sum: {α : Type ?u.169} → [inst : Add α] → [inst : Zero α] → List α → α
sum
:
α: Type ?u.89
α
) = (s.
map: {α : Type ?u.275} → {β : Type ?u.274} → (α → β) → List α → List β
map
(↑): ℚ → α
(↑)
).
sum: {α : Type ?u.283} → [inst : Add α] → [inst : Zero α] → List α → α
sum
:=
map_list_sum: ∀ {M : Type ?u.741} {N : Type ?u.742} [inst : AddMonoid M] [inst_1 : AddMonoid N] {F : Type ?u.740} [inst_2 : AddMonoidHomClass F M N] (f : F) (l : List M), ↑f (List.sum l) = List.sum (List.map (↑f) l)
map_list_sum
(
Rat.castHom: (α : Type ?u.749) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom
α: Type ?u.89
α
)
_: List ?m.743
_
#align rat.cast_list_sum
Rat.cast_list_sum: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : List ℚ), ↑(List.sum s) = List.sum (List.map Rat.cast s)
Rat.cast_list_sum
@[simp, norm_cast] theorem
cast_multiset_sum: ∀ (s : Multiset ℚ), ↑(Multiset.sum s) = Multiset.sum (Multiset.map Rat.cast s)
cast_multiset_sum
(s :
Multiset: Type ?u.1193 → Type ?u.1193
Multiset
ℚ: Type
ℚ
) : (↑s.
sum: {α : Type ?u.1198} → [inst : AddCommMonoid α] → Multiset α → α
sum
:
α: Type ?u.1118
α
) = (s.
map: {α : Type ?u.1269} → {β : Type ?u.1268} → (α → β) → Multiset α → Multiset β
map
(↑): ℚ → α
(↑)
).
sum: {α : Type ?u.1277} → [inst : AddCommMonoid α] → Multiset α → α
sum
:=
map_multiset_sum: ∀ {α : Type ?u.1597} {β : Type ?u.1598} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {F : Type ?u.1599} [inst_2 : AddMonoidHomClass F α β] (f : F) (s : Multiset α), ↑f (Multiset.sum s) = Multiset.sum (Multiset.map (↑f) s)
map_multiset_sum
(
Rat.castHom: (α : Type ?u.1606) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom
α: Type ?u.1118
α
)
_: Multiset ?m.1600
_
#align rat.cast_multiset_sum
Rat.cast_multiset_sum: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : Multiset ℚ), ↑(Multiset.sum s) = Multiset.sum (Multiset.map Rat.cast s)
Rat.cast_multiset_sum
@[simp, norm_cast] theorem
cast_sum: ∀ (s : Finset ι) (f : ι → ℚ), ↑(∑ i in s, f i) = ∑ i in s, ↑(f i)
cast_sum
(
s: Finset ι
s
:
Finset: Type ?u.2197 → Type ?u.2197
Finset
ι: Type ?u.2119
ι
) (
f: ι → ℚ
f
:
ι: Type ?u.2119
ι
→
ℚ: Type
ℚ
) : (∑
i: ?m.2213
i
in
s: Finset ι
s
,
f: ι → ℚ
f
i: ?m.2213
i
) = ∑
i: ?m.2234
i
in
s: Finset ι
s
, (
f: ι → ℚ
f
i: ?m.2234
i
:
α: Type ?u.2122
α
) := (
map_sum: ∀ {β : Type ?u.10556} {α : Type ?u.10555} {γ : Type ?u.10554} [inst : AddCommMonoid β] [inst_1 : AddCommMonoid γ] {G : Type ?u.10557} [inst_2 : AddMonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α), ↑g (∑ x in s, f x) = ∑ x in s, ↑g (f x)
map_sum
(
Rat.castHom: (α : Type ?u.10565) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom
α: Type ?u.2122
α
)
_: ?m.10559 → ?m.10558
_
s: Finset ι
s
) #align rat.cast_sum
Rat.cast_sum: ∀ {ι : Type u_1} {α : Type u_2} [inst : DivisionRing α] [inst_1 : CharZero α] (s : Finset ι) (f : ι → ℚ), ↑(∑ i in s, f i) = ∑ i in s, ↑(f i)
Rat.cast_sum
@[simp, norm_cast] theorem
cast_list_prod: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : List ℚ), ↑(List.prod s) = List.prod (List.map Rat.cast s)
cast_list_prod
(s :
List: Type ?u.11175 → Type ?u.11175
List
ℚ: Type
ℚ
) : (↑s.
prod: {α : Type ?u.11180} → [inst : Mul α] → [inst : One α] → List α → α
prod
:
α: Type ?u.11100
α
) = (s.
map: {α : Type ?u.11279} → {β : Type ?u.11278} → (α → β) → List α → List β
map
(↑): ℚ → α
(↑)
).
prod: {α : Type ?u.11287} → [inst : Mul α] → [inst : One α] → List α → α
prod
:=
map_list_prod: ∀ {M : Type ?u.11659} {N : Type ?u.11660} [inst : Monoid M] [inst_1 : Monoid N] {F : Type ?u.11658} [inst_2 : MonoidHomClass F M N] (f : F) (l : List M), ↑f (List.prod l) = List.prod (List.map (↑f) l)
map_list_prod
(
Rat.castHom: (α : Type ?u.11667) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom
α: Type ?u.11100
α
)
_: List ?m.11661
_
#align rat.cast_list_prod
Rat.cast_list_prod: ∀ {α : Type u_1} [inst : DivisionRing α] [inst_1 : CharZero α] (s : List ℚ), ↑(List.prod s) = List.prod (List.map Rat.cast s)
Rat.cast_list_prod
end WithDivRing section Field variable [
Field: Type ?u.12998 → Type ?u.12998
Field
α: Type ?u.12141
α
] [
CharZero: (R : Type ?u.12147) → [inst : AddMonoidWithOne R] → Prop
CharZero
α: Type ?u.12141
α
] @[simp, norm_cast] theorem
cast_multiset_prod: ∀ (s : Multiset ℚ), ↑(Multiset.prod s) = Multiset.prod (Multiset.map Rat.cast s)
cast_multiset_prod
(s :
Multiset: Type ?u.12304 → Type ?u.12304
Multiset
ℚ: Type
ℚ
) : (↑s.
prod: {α : Type ?u.12309} → [inst : CommMonoid α] → Multiset α → α
prod
:
α: Type ?u.12224
α
) = (s.
map: {α : Type ?u.12375} → {β : Type ?u.12374} → (α → β) → Multiset α → Multiset β
map
(↑): ℚ → α
(↑)
).
prod: {α : Type ?u.12383} → [inst : CommMonoid α] → Multiset α → α
prod
:=
map_multiset_prod: ∀ {α : Type ?u.12575} {β : Type ?u.12576} [inst : CommMonoid α] [inst_1 : CommMonoid β] {F : Type ?u.12577} [inst_2 : MonoidHomClass F α β] (f : F) (s : Multiset α), ↑f (Multiset.prod s) = Multiset.prod (Multiset.map (↑f) s)
map_multiset_prod
(
Rat.castHom: (α : Type ?u.12584) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom
α: Type ?u.12224
α
)
_: Multiset ?m.12578
_
#align rat.cast_multiset_prod
Rat.cast_multiset_prod: ∀ {α : Type u_1} [inst : Field α] [inst_1 : CharZero α] (s : Multiset ℚ), ↑(Multiset.prod s) = Multiset.prod (Multiset.map Rat.cast s)
Rat.cast_multiset_prod
@[simp, norm_cast] theorem
cast_prod: ∀ (s : Finset ι) (f : ι → ℚ), ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
cast_prod
(
s: Finset ι
s
:
Finset: Type ?u.13075 → Type ?u.13075
Finset
ι: Type ?u.12992
ι
) (
f: ι → ℚ
f
:
ι: Type ?u.12992
ι
→
ℚ: Type
ℚ
) : (∏
i: ?m.13091
i
in
s: Finset ι
s
,
f: ι → ℚ
f
i: ?m.13091
i
) = ∏
i: ?m.13114
i
in
s: Finset ι
s
, (
f: ι → ℚ
f
i: ?m.13114
i
:
α: Type ?u.12995
α
) :=
map_prod: ∀ {β : Type ?u.21298} {α : Type ?u.21297} {γ : Type ?u.21296} [inst : CommMonoid β] [inst_1 : CommMonoid γ] {G : Type ?u.21299} [inst_2 : MonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α), ↑g (∏ x in s, f x) = ∏ x in s, ↑g (f x)
map_prod
(
Rat.castHom: (α : Type ?u.21307) → [inst : DivisionRing α] → [inst_1 : CharZero α] → ℚ →+* α
Rat.castHom
α: Type ?u.12995
α
)
_: ?m.21301 → ?m.21300
_
_: Finset ?m.21301
_
#align rat.cast_prod
Rat.cast_prod: ∀ {ι : Type u_1} {α : Type u_2} [inst : Field α] [inst_1 : CharZero α] (s : Finset ι) (f : ι → ℚ), ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
Rat.cast_prod
end Field end Rat