Theorems · Theorem · field theory

Polynomial.eq_of_natDegree_lt_card_of_eval_eq

∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (p q : Polynomial R) {ι : Type u_2} [inst_2 : Fintype ι] {f : ι → R},
  Function.Injective f →
    (∀ (i : ι), Polynomial.eval (f i) p = Polynomial.eval (f i) q) →
      max p.natDegree q.natDegree < Fintype.card ι → p = q

Defined in: Mathlib.Algebra.Polynomial.Roots
Cited by: 1 results in Mathlib
Foundations: Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDomain Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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
Fintypestatement and proof · cited by 7,736
Polynomialstatement and proof · cited by 5,681
IsDomainstatement and proof · cited by 2,196
Fintype.cardstatement and proof · cited by 1,386
Polynomial.natDegreestatement and proof · cited by 1,105
Polynomial.evalstatement and proof · cited by 796
sub_eq_zeroproof · cited by 407
Polynomial.eval_subproof · cited by 124
Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zeroproof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.eq_of_natDegree_lt_card_of_eval_eq'proof · cited by 0