Theorems · Theorem · commutative algebra

WittVector.sum_coeff_eq_coeff_sum

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [inst : CommRing R] {α : Type u_2} {S : Finset α}
  (x : α → WittVector p R),
  (∀ (n : ℕ), Subsingleton ↑{r | r ∈ S ∧ (x r).coeff n ≠ 0}) →
    ∀ (n : ℕ), (∑ s ∈ S, x s).coeff n = ∑ s ∈ S, (x s).coeff n

Defined in

Mathlib.RingTheory.WittVector.TeichmullerSeries

Cited by

1 results in Mathlib

Foundations

Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactCommRing