Theorems · Theorem · commutative algebra

Fin.accumulate_rec

∀ {i n m : ℕ} (hin : i < n) (him : i + 1 < m) (t : Fin n → ℕ),
  (Fin.accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩ + (Fin.accumulate n m) t ⟨i + 1, him⟩

Defined in

Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Cited by

2 results in Mathlib

Foundations

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