Lagrange

📁 Source: Mathlib/LinearAlgebra/Lagrange.lean

Statistics

Metric	Count
Definitions basis, basisDivisor, funEquivDegreeLT, interpolate, nodal, nodalWeight	6
Theorems X_sub_C_dvd_nodal, basisDivisor_add_symm, basisDivisor_eq_zero_iff, basisDivisor_inj, basisDivisor_ne_zero_iff, basisDivisor_self, basis_empty, basis_eq_prod_sub_inv_mul_nodal_div, basis_ne_zero, basis_pair_left, basis_pair_right, basis_singleton, coeff_eq_sum, degree_basis, degree_basisDivisor_of_ne, degree_basisDivisor_self, degree_interpolate_erase_lt, degree_interpolate_le, degree_interpolate_lt, degree_nodal, derivative_nodal, eq_interpolate, eq_interpolate_iff, eq_interpolate_of_eval_eq, eval_basisDivisor_left_of_ne, eval_basisDivisor_right, eval_basis_not_at_node, eval_basis_of_ne, eval_basis_self, eval_interpolate_at_node, eval_interpolate_not_at_node, eval_interpolate_not_at_node', eval_iterate_derivative_eq_sum, eval_nodal, eval_nodal_at_node, eval_nodal_derivative_eval_node_eq, eval_nodal_not_at_node, interpolate_apply, interpolate_empty, interpolate_eq_add_interpolate_erase, interpolate_eq_iff_values_eq_on, interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, interpolate_eq_of_values_eq_on, interpolate_eq_sum, interpolate_eq_sum_interpolate_insert_sdiff, interpolate_one, interpolate_poly_eq_self, interpolate_singleton, iterate_derivative_interpolate, leadingCoeff_basis, leadingCoeff_eq_sum, natDegree_basis, natDegree_basisDivisor_of_ne, natDegree_basisDivisor_self, natDegree_nodal, nodalWeight_eq_eval_derivative_nodal, nodalWeight_eq_eval_nodal_erase_inv, nodalWeight_ne_zero, nodal_empty, nodal_eq, nodal_eq_mul_nodal_erase, nodal_erase_eq_nodal_div, nodal_insert_eq_nodal, nodal_monic, nodal_ne_zero, nodal_subgroup_eq_X_pow_card_sub_one, sum_basis, sum_nodalWeight_mul_inv_sub_ne_zero, values_eq_on_of_interpolate_eq, eq_of_degree_le_of_eval_finset_eq, eq_of_degree_le_of_eval_index_eq, eq_of_degree_sub_lt_of_eval_finset_eq, eq_of_degree_sub_lt_of_eval_index_eq, eq_of_degrees_lt_of_eval_finset_eq, eq_of_degrees_lt_of_eval_index_eq, eq_zero_of_degree_lt_of_eval_finset_eq_zero, eq_zero_of_degree_lt_of_eval_index_eq_zero	77
Total	83

Lagrange

Definitions

Name	Category	Theorems
basis 📖	CompOp	14 math math: basis_pair_right, leadingCoeff_basis, interpolate_eq_sum_interpolate_insert_sdiff, basis_singleton, basis_eq_prod_sub_inv_mul_nodal_div, basis_empty, degree_basis, eval_basis_of_ne, interpolate_apply, sum_basis, eval_basis_self, natDegree_basis, basis_pair_left, eval_basis_not_at_node
basisDivisor 📖	CompOp	12 math math: basis_pair_right, degree_basisDivisor_self, basisDivisor_self, basisDivisor_add_symm, eval_basisDivisor_right, degree_basisDivisor_of_ne, basisDivisor_eq_zero_iff, natDegree_basisDivisor_self, eval_basisDivisor_left_of_ne, natDegree_basisDivisor_of_ne, interpolate_eq_add_interpolate_erase, basis_pair_left
funEquivDegreeLT 📖	CompOp	—
interpolate 📖	CompOp	21 math math: interpolate_one, interpolate_eq_of_values_eq_on, eval_interpolate_not_at_node', eval_interpolate_not_at_node, interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, interpolate_eq_sum_interpolate_insert_sdiff, eq_interpolate_iff, interpolate_eq_sum, degree_interpolate_erase_lt, degree_interpolate_lt, eq_interpolate, iterate_derivative_interpolate, degree_interpolate_le, interpolate_eq_add_interpolate_erase, interpolate_apply, interpolate_eq_iff_values_eq_on, interpolate_empty, eq_interpolate_of_eval_eq, eval_interpolate_at_node, interpolate_poly_eq_self, interpolate_singleton
nodal 📖	CompOp	20 math math: nodalWeight_eq_eval_nodal_erase_inv, derivative_nodal, eval_interpolate_not_at_node, interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, nodal_insert_eq_nodal, natDegree_nodal, nodal_empty, eval_nodal_at_node, basis_eq_prod_sub_inv_mul_nodal_div, eval_nodal, X_sub_C_dvd_nodal, degree_nodal, nodal_eq_mul_nodal_erase, nodal_monic, eval_nodal_derivative_eval_node_eq, nodal_subgroup_eq_X_pow_card_sub_one, nodal_erase_eq_nodal_div, nodal_eq, nodalWeight_eq_eval_derivative_nodal, eval_basis_not_at_node
nodalWeight 📖	CompOp	7 math math: eval_interpolate_not_at_node', nodalWeight_eq_eval_nodal_erase_inv, eval_interpolate_not_at_node, interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, basis_eq_prod_sub_inv_mul_nodal_div, nodalWeight_eq_eval_derivative_nodal, eval_basis_not_at_node

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_sub_C_dvd_nodal 📖	mathematical	Finset Finset.instMembership	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C nodal	—	nodal_eq_mul_nodal_erase
basisDivisor_add_symm 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instAdd basisDivisor Polynomial.instOne	—	sum_basis Function.Injective.injOn Finset.mem_insert_self Finset.sum_insert Finset.notMem_singleton Finset.sum_singleton basis_pair_left basis_pair_right
basisDivisor_eq_zero_iff 📖	mathematical	—	basisDivisor Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instZero	—	basisDivisor_self
basisDivisor_inj 📖	—	basisDivisor Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instZero	—	—	EuclideanDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
basisDivisor_ne_zero_iff 📖	—	—	—	—	basisDivisor_eq_zero_iff
basisDivisor_self 📖	mathematical	—	basisDivisor Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instZero	—	sub_self inv_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul
basis_empty 📖	mathematical	—	basis Finset Finset.instEmptyCollection Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instOne	—	—
basis_eq_prod_sub_inv_mul_nodal_div 📖	mathematical	Finset Finset.instMembership	basis Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C nodalWeight Polynomial.instDiv nodal Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.X	—	Finset.prod_congr Finset.prod_mul_distrib map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass nodal_erase_eq_nodal_div
basis_ne_zero 📖	—	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	—	—	Polynomial.nontrivial EuclideanDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain basisDivisor_eq_zero_iff Set.InjOn.eq_iff
basis_pair_left 📖	mathematical	—	basis Finset Finset.instInsert Finset.instSingleton basisDivisor	—	Finset.prod_congr Finset.erase_insert_eq_erase Finset.erase_eq_of_notMem Finset.prod_singleton
basis_pair_right 📖	mathematical	—	basis Finset Finset.instInsert Finset.instSingleton basisDivisor	—	Finset.pair_comm basis_pair_left
basis_singleton 📖	mathematical	—	basis Finset Finset.instSingleton Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instOne	—	basis.eq_1 Finset.erase_singleton Finset.prod_empty
coeff_eq_sum 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	Polynomial.coeff Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Polynomial.eval Finset.prod CommRing.toCommMonoid Finset.erase SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing	—	eq_interpolate interpolate_apply Polynomial.finset_sum_coeff Finset.sum_congr Polynomial.coeff_C_mul natDegree_basis Polynomial.leadingCoeff.eq_1 leadingCoeff_basis Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ one_ne_zero NeZero.one GroupWithZero.toNontrivial
degree_basis 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basis WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	—	Polynomial.degree_eq_natDegree basis_ne_zero natDegree_basis
degree_basisDivisor_of_ne 📖	mathematical	—	Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basisDivisor WithBot WithBot.one Nat.instOne	—	basisDivisor.eq_1 Polynomial.degree_mul IsDomain.to_noZeroDivisors instIsDomain Polynomial.degree_X_sub_C EuclideanDomain.toNontrivial Polynomial.degree_C inv_ne_zero sub_ne_zero_of_ne zero_add
degree_basisDivisor_self 📖	mathematical	—	Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basisDivisor Bot.bot WithBot WithBot.bot	—	basisDivisor_self Polynomial.degree_zero
degree_interpolate_erase_lt 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Finset.erase AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	—	Finset.card_erase_of_mem degree_interpolate_lt Set.InjOn.mono Finset.coe_subset Finset.erase_subset
degree_interpolate_le 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	—	LE.le.trans Polynomial.degree_sum_le Finset.sup_le_iff Polynomial.degree_mul IsDomain.to_noZeroDivisors instIsDomain degree_basis map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass bot_le Polynomial.degree_C zero_add le_refl
degree_interpolate_lt 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	—	Nat.cast_withBot Finset.eq_empty_or_nonempty interpolate_empty Polynomial.degree_zero Finset.card_empty WithBot.bot_lt_coe lt_of_le_of_lt degree_interpolate_le WithBot.coe_lt_coe Finset.Nonempty.card_pos zero_lt_one Nat.instZeroLEOneClass
degree_nodal 📖	mathematical	—	Polynomial.degree CommSemiring.toSemiring CommRing.toCommSemiring nodal WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	—	Polynomial.degree_eq_natDegree nodal_ne_zero natDegree_nodal
derivative_nodal 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative nodal Finset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Finset.erase	—	Finset.induction_on nodal_empty Polynomial.derivative_one Finset.sum_empty nodal_insert_eq_nodal Polynomial.derivative_mul Polynomial.derivative_sub Polynomial.derivative_X Polynomial.derivative_C sub_zero one_mul Finset.sum_insert Finset.mul_sum Finset.erase_insert AddLeftCancelSemigroup.toIsLeftCancelAdd Finset.sum_congr Finset.erase_insert_of_ne Function.mt Finset.mem_of_mem_erase
eq_interpolate 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Polynomial.eval	—	Polynomial.eq_of_degrees_lt_of_eval_index_eq instIsDomain degree_interpolate_lt eval_interpolate_at_node
eq_interpolate_iff 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card Polynomial.eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate	—	eq_interpolate_of_eval_eq degree_interpolate_lt eval_interpolate_at_node
eq_interpolate_of_eval_eq 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card Polynomial.eval	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate	—	eq_interpolate interpolate_eq_of_values_eq_on
eval_basisDivisor_left_of_ne 📖	mathematical	—	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basisDivisor AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_sub Polynomial.eval_X inv_mul_cancel₀ sub_ne_zero_of_ne
eval_basisDivisor_right 📖	mathematical	—	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basisDivisor MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_sub Polynomial.eval_X sub_self MulZeroClass.mul_zero
eval_basis_not_at_node 📖	mathematical	Finset Finset.instMembership	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basis Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring CommRing.toCommSemiring nodal nodalWeight InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	mul_comm basis_eq_prod_sub_inv_mul_nodal_div Polynomial.eval_mul Polynomial.eval_C nodal_erase_eq_nodal_div eval_nodal mul_assoc Finset.mul_prod_erase inv_mul_cancel₀ sub_ne_zero_of_ne one_mul
eval_basis_of_ne 📖	mathematical	Finset Finset.instMembership	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basis MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Polynomial.eval_prod EuclideanDomain.toNontrivial IsDomain.to_noZeroDivisors instIsDomain Finset.mem_erase eval_basisDivisor_right
eval_basis_self 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basis AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	basis.eq_1 Polynomial.eval_prod Finset.prod_eq_one eval_basisDivisor_left_of_ne Finset.mem_erase
eval_interpolate_at_node 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate	—	interpolate_apply Polynomial.eval_finset_sum Finset.add_sum_erase Polynomial.eval_mul Finset.sum_congr Polynomial.eval_C eval_basis_self mul_one AddLeftCancelSemigroup.toIsLeftCancelAdd Finset.sum_eq_zero eval_basis_of_ne Finset.mem_erase MulZeroClass.mul_zero
eval_interpolate_not_at_node 📖	mathematical	—	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Distrib.toMul NonUnitalNonAssocSemiring.toDistrib CommSemiring.toSemiring CommRing.toCommSemiring nodal Finset.sum nodalWeight InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Finset.mul_sum Polynomial.eval_finset_sum Finset.sum_congr Polynomial.eval_mul Polynomial.eval_C mul_assoc mul_comm eval_basis_not_at_node
eval_interpolate_not_at_node' 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.Nonempty	Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Finset.sum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib nodalWeight InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing	—	div_one Polynomial.eval_one interpolate_one eval_interpolate_not_at_node Finset.sum_congr mul_one mul_div_mul_left eval_nodal_not_at_node EuclideanDomain.toNontrivial IsDomain.to_noZeroDivisors instIsDomain
eval_iterate_derivative_eq_sum 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	Polynomial.eval Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Finset.sum DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Finset.prod CommRing.toCommMonoid Finset.erase SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Finset.powersetCard	—	eq_interpolate iterate_derivative_interpolate Polynomial.eval_mul Polynomial.eval_natCast Polynomial.eval_finset_sum Finset.sum_congr Polynomial.eval_C Polynomial.eval_prod Finset.prod_congr Polynomial.eval_sub Polynomial.eval_X
eval_nodal 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring nodal Finset.prod CommRing.toCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	Polynomial.eval_prod Finset.prod_congr Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_C
eval_nodal_at_node 📖	mathematical	Finset Finset.instMembership	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring nodal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eval_nodal Finset.prod_eq_zero sub_self
eval_nodal_derivative_eval_node_eq 📖	mathematical	Finset Finset.instMembership	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative nodal Finset.erase	—	derivative_nodal Polynomial.eval_finset_sum Finset.add_sum_erase add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd Finset.sum_eq_zero eval_nodal_at_node Finset.mem_erase
eval_nodal_not_at_node 📖	—	—	—	—	Polynomial.eval_prod Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_C
interpolate_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Finset.sum Polynomial.instMul RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C basis	—	—
interpolate_empty 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Finset Finset.instEmptyCollection Polynomial.instZero	—	interpolate_apply Finset.sum_empty
interpolate_eq_add_interpolate_erase 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Polynomial.instAdd Polynomial.instMul Finset.erase basisDivisor	—	interpolate_eq_sum_interpolate_insert_sdiff Finset.mem_insert_self Finset.insert_subset_iff Finset.singleton_subset_iff Finset.sum_insert Finset.notMem_singleton Finset.sum_singleton basis_pair_left basis_pair_right Finset.sdiff_insert_insert_of_mem_of_notMem Finset.sdiff_singleton_eq_erase Finset.pair_comm
interpolate_eq_iff_values_eq_on 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate	—	values_eq_on_of_interpolate_eq interpolate_eq_of_values_eq_on
interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Finset.sum Polynomial.instMul CommSemiring.toSemiring CommRing.toCommSemiring RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C nodalWeight Polynomial.instDiv nodal Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.X	—	Finset.sum_congr mul_comm basis_eq_prod_sub_inv_mul_nodal_div
interpolate_eq_of_values_eq_on 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate	—	Finset.sum_congr
interpolate_eq_sum 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Finset.sum Polynomial.instMul RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Finset.prod CommRing.toCommMonoid Finset.erase SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Polynomial.instSub Polynomial.X	—	Finset.sum_congr Finset.prod_congr Finset.prod_mul_distrib MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_eq_mul_inv map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_assoc
interpolate_eq_sum_interpolate_insert_sdiff 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.Nonempty Finset.instHasSubset	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Finset.sum Polynomial.instMul Finset.instInsert Finset.instSDiff basis	—	eq_interpolate_of_eval_eq lt_of_le_of_lt Polynomial.degree_sum_le Finset.sup_lt_iff WithBot.bot_lt_coe Polynomial.degree_mul IsDomain.to_noZeroDivisors instIsDomain Finset.Nonempty.card_pos Finset.card_le_card add_assoc tsub_add_tsub_cancel CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub add_tsub_assoc_of_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le LE.le.trans zero_add degree_basis Set.InjOn.mono WithBot.coe_add Nat.cast_withBot WithBot.add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add WithBot.coe_ne_bot Finset.card_insert_of_notMem Finset.notMem_sdiff_of_mem_right Finset.card_sdiff_of_subset add_comm degree_interpolate_lt Finset.coe_subset Finset.insert_subset_iff Finset.sdiff_subset Polynomial.eval_finset_sum Finset.sum_congr Polynomial.eval_mul Finset.add_sum_erase eval_basis_self eval_interpolate_at_node Finset.mem_insert_self mul_one add_eq_left Finset.sum_eq_zero Finset.mem_erase eval_basis_of_ne MulZeroClass.mul_zero sum_basis Polynomial.eval_one Finset.mul_sum Finset.mem_insert Finset.mem_sdiff
interpolate_one 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.Nonempty	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Polynomial.instOne	—	Finset.sum_congr map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul sum_basis
interpolate_poly_eq_self 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Polynomial.eval	—	eq_interpolate
interpolate_singleton 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Finset Finset.instSingleton RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C	—	interpolate_apply Finset.sum_singleton basis_singleton mul_one
iterate_derivative_interpolate 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.card	Nat.iterate Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative Pi.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module interpolate Polynomial.instMul Polynomial.instNatCast Nat.factorial Finset.sum RingHom RingHom.instFunLike Polynomial.C DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Finset.prod CommRing.toCommMonoid Finset.erase SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Finset.powersetCard Polynomial.instSub Polynomial.X	—	interpolate_eq_sum Polynomial.iterate_derivative_sum Finset.sum_congr Polynomial.iterate_derivative_C_mul Finset.mul_sum mul_comm mul_assoc Set.InjOn.mono Finset.coe_subset Finset.erase_subset Finset.prod_image Finset.powersetCard_eq_filter Finset.powerset_image Finset.sum_nbij Finset.image_injOn_powerset_of_injOn
leadingCoeff_basis 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	Polynomial.leadingCoeff DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basis InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Finset.prod CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Finset.erase SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Polynomial.natDegree_finset_prod_X_sub_C_eq_card EuclideanDomain.toNontrivial Finset.card_erase_of_mem Polynomial.Monic.coeff_natDegree Polynomial.monic_prod_X_sub_C natDegree_basis Finset.prod_congr Finset.prod_mul_distrib MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.prod_inv_distrib Polynomial.coeff_C_mul mul_one
leadingCoeff_eq_sum 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card WithBot.add Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot.one Nat.instOne	Polynomial.leadingCoeff Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Polynomial.eval Finset.prod CommRing.toCommMonoid Finset.erase SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing	—	CanLift.prf WithBot.canLift Mathlib.Tactic.Contrapose.contrapose₃ WithBot.coe_eq_coe WithBot.coe_add WithBot.coe_one Polynomial.leadingCoeff.eq_1 Polynomial.natDegree_eq_of_degree_eq_some coeff_eq_sum WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero
natDegree_basis 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basis Finset.card	—	Finset.card_erase_of_mem Finset.card_eq_sum_ones Finset.sum_congr natDegree_basisDivisor_of_ne basisDivisor_eq_zero_iff Polynomial.natDegree_prod IsDomain.to_noZeroDivisors instIsDomain
natDegree_basisDivisor_of_ne 📖	mathematical	—	Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basisDivisor	—	Polynomial.natDegree_eq_of_degree_eq_some degree_basisDivisor_of_ne
natDegree_basisDivisor_self 📖	mathematical	—	Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield basisDivisor	—	basisDivisor_self Polynomial.natDegree_zero
natDegree_nodal 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring nodal Finset.card	—	Polynomial.natDegree_prod_of_monic Polynomial.monic_X_sub_C Finset.sum_congr Polynomial.natDegree_X_sub_C Finset.sum_const mul_one
nodalWeight_eq_eval_derivative_nodal 📖	mathematical	Finset Finset.instMembership	nodalWeight InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative nodal	—	eval_nodal_derivative_eval_node_eq nodalWeight_eq_eval_nodal_erase_inv
nodalWeight_eq_eval_nodal_erase_inv 📖	mathematical	—	nodalWeight InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain nodal Finset.erase	—	eval_nodal nodalWeight.eq_1 Finset.prod_inv_distrib
nodalWeight_ne_zero 📖	—	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.instMembership	—	—	nodalWeight.eq_1 Finset.prod_ne_zero_iff EuclideanDomain.toNontrivial IsDomain.to_noZeroDivisors instIsDomain Finset.mem_erase inv_ne_zero sub_ne_zero_of_ne Set.InjOn.eq_iff
nodal_empty 📖	mathematical	—	nodal Finset Finset.instEmptyCollection Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne	—	—
nodal_eq 📖	mathematical	—	nodal Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	—
nodal_eq_mul_nodal_erase 📖	mathematical	Finset Finset.instMembership	nodal Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Finset.erase	—	Finset.mul_prod_erase
nodal_erase_eq_nodal_div 📖	mathematical	Finset Finset.instMembership	nodal EuclideanDomain.toCommRing Field.toEuclideanDomain Finset.erase Polynomial CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instDiv Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	nodal_eq_mul_nodal_erase mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Polynomial.X_sub_C_ne_zero EuclideanDomain.toNontrivial
nodal_insert_eq_nodal 📖	mathematical	Finset Finset.instMembership	nodal Finset.instInsert Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	Finset.prod_insert
nodal_monic 📖	mathematical	—	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring nodal	—	Polynomial.monic_prod_of_monic Polynomial.monic_X_sub_C
nodal_ne_zero 📖	—	—	—	—	Finset.eq_empty_or_nonempty one_ne_zero NeZero.one Polynomial.nontrivial Polynomial.ne_zero_of_natDegree_gt natDegree_nodal Finset.Nonempty.card_pos
nodal_subgroup_eq_X_pow_card_sub_one 📖	mathematical	—	nodal Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Set.toFinset SetLike.coe Subgroup Units.instGroup Subgroup.instSetLike Units.val Polynomial Polynomial.instSub CommRing.toRing Monoid.toNatPow Polynomial.semiring Polynomial.X Fintype.card SetLike.instMembership Polynomial.instOne	—	Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instNontrivial Polynomial.degree_one IsDomain.toNontrivial Polynomial.degree_pow IsDomain.to_noZeroDivisors Polynomial.degree_X nsmul_eq_mul mul_one WithBot.instIsOrderedRing IsStrictOrderedRing.toIsOrderedRing WithBot.nontrivial One.instNonempty Polynomial.eq_of_degree_le_of_eval_index_eq Function.Injective.injOn Units.val_injective degree_nodal Set.toFinset_card Polynomial.degree_sub_eq_left_of_degree_lt WithBot.charZero Nat.instCharZero nodal_monic Polynomial.leadingCoeff_sub_of_degree_lt Polynomial.monic_X_pow eval_nodal_at_node Polynomial.eval_sub Polynomial.eval_pow Polynomial.eval_X pow_card_eq_one Polynomial.eval_one sub_self
sum_basis 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.Nonempty	Finset.sum Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain basis Polynomial.instOne	—	Polynomial.eq_of_degrees_lt_of_eval_index_eq instIsDomain lt_of_le_of_lt Polynomial.degree_sum_le Nat.cast_withBot Finset.sup_lt_iff WithBot.bot_lt_coe degree_basis WithBot.coe_lt_coe Finset.card_ne_zero_of_mem Polynomial.degree_one EuclideanDomain.toNontrivial WithBot.coe_zero Finset.Nonempty.card_pos Polynomial.eval_finset_sum Polynomial.eval_one Finset.add_sum_erase eval_basis_self add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd Finset.sum_eq_zero Finset.mem_erase eval_basis_of_ne
sum_nodalWeight_mul_inv_sub_ne_zero 📖	—	Set.InjOn SetLike.coe Finset Finset.instSetLike Finset.Nonempty	—	—	right_ne_zero_of_mul_eq_one EuclideanDomain.toNontrivial Finset.sum_congr mul_one interpolate_one Polynomial.eval_one eval_interpolate_not_at_node
values_eq_on_of_interpolate_eq 📖	—	Set.InjOn SetLike.coe Finset Finset.instSetLike DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.commRing Pi.Function.module Semiring.toModule Polynomial.module LinearMap.instFunLike interpolate Finset.instMembership	—	—	eval_interpolate_at_node

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_degree_le_of_eval_finset_eq 📖	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card leadingCoeff eval	—	—	eq_or_ne degree_eq_bot degree_zero eq_of_degree_sub_lt_of_eval_finset_eq lt_of_lt_of_le degree_sub_lt
eq_of_degree_le_of_eval_index_eq 📖	—	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card leadingCoeff eval	—	—	eq_or_ne degree_eq_bot degree_zero eq_of_degree_sub_lt_of_eval_index_eq lt_of_lt_of_le degree_sub_lt
eq_of_degree_sub_lt_of_eval_finset_eq 📖	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring Polynomial instSub CommRing.toRing AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card eval	—	—	sub_eq_zero eq_zero_of_degree_lt_of_eval_finset_eq_zero eval_sub
eq_of_degree_sub_lt_of_eval_index_eq 📖	—	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring Polynomial instSub CommRing.toRing AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card eval	—	—	sub_eq_zero eq_zero_of_degree_lt_of_eval_index_eq_zero eval_sub
eq_of_degrees_lt_of_eval_finset_eq 📖	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card eval	—	—	eq_of_degree_sub_lt_of_eval_finset_eq mem_degreeLT Submodule.sub_mem
eq_of_degrees_lt_of_eval_index_eq 📖	—	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card eval	—	—	eq_of_degree_sub_lt_of_eval_index_eq mem_degreeLT Submodule.sub_mem
eq_zero_of_degree_lt_of_eval_finset_eq_zero 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Polynomial instZero	—	RingHomInvPair.ids mem_degreeLT degreeLTEquiv_eq_zero_iff_eq_zero Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero Fintype.card_coe Function.Embedding.inj' Equiv.injective eval_eq_sum_degreeLTEquiv Finset.coe_mem
eq_zero_of_degree_lt_of_eval_index_eq_zero 📖	mathematical	Set.InjOn SetLike.coe Finset Finset.instSetLike WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Finset.card eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Polynomial instZero	—	eq_zero_of_degree_lt_of_eval_finset_eq_zero Finset.card_image_of_injOn Finset.mem_image

---

← Back to Index