Theorems · Theorem · linear algebra

Polynomial.eq_of_degree_le_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 →
      f.degree = g.degree →
        f.leadingCoeff = g.leadingCoeff → (∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g) → f = g

Defined in: Mathlib.LinearAlgebra.Lagrange
Cited by: 1 results in Mathlib
Foundations: Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDomain

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites17

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

CommRingstatement and proof · cited by 17,173
Finsetstatement and proof · cited by 13,712
SetLike.coestatement and proof · cited by 8,199
Polynomialstatement and proof · cited by 5,681
Finset.cardstatement and proof · cited by 2,327
IsDomainstatement and proof · cited by 2,196
WithBotstatement and proof · cited by 1,498
eq_or_neproof · cited by 1,117
Polynomial.evalstatement and proof · cited by 796
Polynomial.degreestatement and proof · cited by 643
Set.InjOnstatement and proof · cited by 543
Polynomial.leadingCoeffstatement and proof · cited by 498

Cited by1

Results whose statement or proof uses this declaration.

Lagrange.nodal_subgroup_eq_X_pow_card_sub_oneproof · cited by 0