Theorems · Theorem · linear algebra

Polynomial.eq_of_degrees_lt_of_eval_index_eq

∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f g : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι),
  Set.InjOn v ↑s →
    f.degree < ↑s.card → g.degree < ↑s.card → (∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g) → f = g

Defined in

Mathlib.LinearAlgebra.Lagrange

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain