Mathlib.Data.Rat.BigOperators

Rat.cast_list_sum theorem

(s : List ℚ) : (↑s.sum : α) = (s.map (↑)).sum

Full source

@[simp, norm_cast]
theorem cast_list_sum (s : List ℚ) : (↑s.sum : α) = (s.map (↑)).sum :=
  map_list_sum (Rat.castHom α) _

Sum Preservation for Lists under Rational Number Casting in Characteristic Zero Rings

Informal description

Let $\alpha$ be a characteristic zero ring. For any list $s$ of rational numbers, the canonical image of the sum of $s$ in $\alpha$ equals the sum of the canonical images of the elements of $s$ in $\alpha$. In symbols: \[ \left(\sum_{x \in s} x\right)_{\alpha} = \sum_{x \in s} (x : \alpha) \]

Rat.cast_multiset_sum theorem

(s : Multiset ℚ) : (↑s.sum : α) = (s.map (↑)).sum

Full source

@[simp, norm_cast]
theorem cast_multiset_sum (s : Multiset ℚ) : (↑s.sum : α) = (s.map (↑)).sum :=
  map_multiset_sum (Rat.castHom α) _

Sum Preservation under Rational Number Casting in Characteristic Zero Fields

Informal description

For any multiset $s$ of rational numbers and any characteristic zero field (or division ring) $\alpha$, the canonical image of the sum of $s$ in $\alpha$ equals the sum of the canonical images of the elements of $s$ in $\alpha$. In symbols: \[ \text{cast}(s.\text{sum}) = \left(\text{map cast } s\right).\text{sum} \]

Rat.cast_sum theorem

(s : Finset ι) (f : ι → ℚ) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : α)

Full source

@[simp, norm_cast]
theorem cast_sum (s : Finset ι) (f : ι → ℚ) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : α) :=
  map_sum (Rat.castHom α) _ s

Sum Preservation under Rational Number Casting in Characteristic Zero Fields

Informal description

Let $\alpha$ be a characteristic zero field (or division ring). For any finite set $s$ and any function $f : \iota \to \mathbb{Q}$, the canonical image of the sum of $f$ over $s$ in $\alpha$ equals the sum of the canonical images of the values of $f$ in $\alpha$. In symbols: \[ \sum_{i \in s} f(i) = \sum_{i \in s} (f(i) : \alpha) \]

Rat.cast_list_prod theorem

(s : List ℚ) : (↑s.prod : α) = (s.map (↑)).prod

Full source

@[simp, norm_cast]
theorem cast_list_prod (s : List ℚ) : (↑s.prod : α) = (s.map (↑)).prod :=
  map_list_prod (Rat.castHom α) _

Product Preservation under Rational Number Casting for Lists in Characteristic Zero Fields

Informal description

Let $\alpha$ be a characteristic zero field (or division ring). For any list $s$ of rational numbers, the canonical image of the product of $s$ in $\alpha$ equals the product of the canonical images of the elements of $s$ in $\alpha$. In symbols: \[ \left(\prod_{x \in s} x\right) = \prod_{x \in s} (x : \alpha) \]

Rat.cast_multiset_prod theorem

(s : Multiset ℚ) : (↑s.prod : α) = (s.map (↑)).prod

Full source

@[simp, norm_cast]
theorem cast_multiset_prod (s : Multiset ℚ) : (↑s.prod : α) = (s.map (↑)).prod :=
  map_multiset_prod (Rat.castHom α) _

Product Preservation under Rational Number Casting in Characteristic Zero Fields for Multisets

Informal description

Let $\alpha$ be a characteristic zero field (or division ring). For any multiset $s$ of rational numbers, the canonical image of the product of $s$ in $\alpha$ equals the product of the canonical images of the elements of $s$ in $\alpha$. In symbols: \[ \left(\prod_{x \in s} x\right) = \prod_{x \in s} (x : \alpha) \]

Rat.cast_prod theorem

(s : Finset ι) (f : ι → ℚ) : ∏ i ∈ s, f i = ∏ i ∈ s, (f i : α)

Full source

@[simp, norm_cast]
theorem cast_prod (s : Finset ι) (f : ι → ℚ) : ∏ i ∈ s, f i = ∏ i ∈ s, (f i : α) :=
  map_prod (Rat.castHom α) _ _

Product Preservation under Rational Number Casting in Characteristic Zero Fields for Finite Sets

Informal description

Let $\alpha$ be a characteristic zero field (or division ring). For any finite set $s$ and function $f : \iota \to \mathbb{Q}$, the canonical image of the product $\prod_{i \in s} f(i)$ in $\alpha$ equals the product of the canonical images $\prod_{i \in s} (f(i) : \alpha)$. In symbols: \[ \left(\prod_{i \in s} f(i)\right) = \prod_{i \in s} (f(i) : \alpha) \]