Casting lemmas for rational numbers involving sums and products #
@[simp]
@[simp]
theorem
Rat.cast_multiset_sum
{α : Type u_2}
[DivisionRing α]
[CharZero α]
(s : Multiset ℚ)
:
↑s.sum = (Multiset.map Rat.cast s).sum
@[simp]
theorem
Rat.cast_sum
{ι : Type u_1}
{α : Type u_2}
[DivisionRing α]
[CharZero α]
(s : Finset ι)
(f : ι → ℚ)
:
↑(s.sum fun (i : ι) => f i) = s.sum fun (i : ι) => ↑(f i)
@[simp]
@[simp]
theorem
Rat.cast_multiset_prod
{α : Type u_2}
[Field α]
[CharZero α]
(s : Multiset ℚ)
:
↑s.prod = (Multiset.map Rat.cast s).prod