English
For x and l, sumsq l x = 0 iff l.Forall (a → a x = 0).
Русский
Для x и l выполняется sumsq l x = 0 тогда и только тогда, когда l.forall (a, a x = 0).
LaTeX
$$$$ \\text{sumsq}(l)(x) = 0 \\iff l.Forall (\\lambda a. a(x) = 0) $$$$
Lean4
/-- Map the index set of variables, replacing `x_i` with `x_(f i)`. -/
def map {α β} (f : α → β) (g : Poly α) : Poly β :=
⟨fun v => g <| v ∘ f,
Poly.induction (C := fun g => IsPoly (fun v => g (v ∘ f))) (fun i => by simpa using IsPoly.proj _)
(fun n => by simpa using IsPoly.const _) (fun f g pf pg => by simpa using IsPoly.sub pf pg)
(fun f g pf pg => by simpa using IsPoly.mul pf pg) _⟩
