Theorems · Theorem · logic and foundations

FirstOrder.Language.presburger.realize_sum

∀ {α : Type u_1} {M : Type u_2} {v : α → M} [inst : AddCommMonoidWithOne M] {β : Type u_3} {s : Finset β}
  {f : β → FirstOrder.Language.presburger.Term α},
  FirstOrder.Language.Term.realize v (FirstOrder.Language.presburger.sum s f) =
    ∑ i ∈ s, FirstOrder.Language.Term.realize v (f i)

Defined in: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommMonoidWithOne

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement and proof · cited by 13,712
Finset.sumstatement and proof · cited by 5,195
FirstOrder.Language.Termstatement and proof · cited by 166
FirstOrder.Language.Term.realizestatement and proof · cited by 81
AddCommMonoidWithOnestatement and proof · cited by 42
Finset.toListproof · cited by 34
FirstOrder.Language.presburgerstatement and proof · cited by 21
Finset.nodup_toListproof · cited by 8
Finset.toList_toFinsetproof · cited by 4
List.sum_toFinsetproof · cited by 4
FirstOrder.Language.presburger.sumstatement · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

IsLinearSet.definableproof · cited by 1