Vandermonde

📁 Source: Mathlib/LinearAlgebra/Vandermonde.lean

Statistics

Metric	Count
Definitions projVandermonde, rectVandermonde, vandermonde	3
Theorems det_eval_matrixOfPolynomials_eq_det_vandermonde, det_projVandermonde, det_vandermonde, det_vandermonde_add, det_vandermonde_eq_zero_iff, det_vandermonde_id_eq_superFactorial, det_vandermonde_ne_zero_iff, det_vandermonde_sub, eq_zero_of_forall_index_sum_mul_pow_eq_zero, eq_zero_of_forall_index_sum_pow_mul_eq_zero, eq_zero_of_forall_pow_sum_mul_pow_eq_zero, eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials, projVandermonde_apply, projVandermonde_apply_of_ne_zero, projVandermonde_apply_zero_right, projVandermonde_comp, projVandermonde_map, rectVandermonde_apply, rectVandermonde_apply_zero_right, superFactorial_dvd_vandermonde_det, vandermonde_apply, vandermonde_cons, vandermonde_eq_projVandermonde, vandermonde_mul_vandermonde_transpose, vandermonde_succ, vandermonde_transpose_mul_vandermonde	26
Total	29

Matrix

Definitions

Name	Category	Theorems
projVandermonde 📖	CompOp	7 math math: det_projVandermonde, vandermonde_eq_projVandermonde, projVandermonde_apply_of_ne_zero, projVandermonde_map, projVandermonde_apply_zero_right, projVandermonde_apply, projVandermonde_comp
rectVandermonde 📖	CompOp	2 math math: rectVandermonde_apply_zero_right, rectVandermonde_apply
vandermonde 📖	CompOp	15 math math: det_vandermonde, vandermonde_succ, det_eval_matrixOfPolynomials_eq_det_vandermonde, vandermonde_eq_projVandermonde, vandermonde_apply, Algebra.embeddingsMatrixReindex_eq_vandermonde, vandermonde_transpose_mul_vandermonde, det_vandermonde_add, vandermonde_mul_vandermonde_transpose, superFactorial_dvd_vandermonde_det, vandermonde_cons, det_vandermonde_id_eq_superFactorial, det_vandermonde_sub, det_vandermonde_eq_zero_iff, eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_eval_matrixOfPolynomials_eq_det_vandermonde 📖	mathematical	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.Monic	det Fin.fintype vandermonde DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike of Polynomial.eval	—	eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials det_mul det_matrixOfPolynomials mul_one
det_projVandermonde 📖	mathematical	—	det Fin.fintype projVandermonde Finset.prod CommRing.toCommMonoid Finset.univ Finset.Ioi PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderTop SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MvPolynomial.instIsDomainOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Int.instIsDomain MvPolynomial.eval₂_mul MvPolynomial.eval₂_pow MvPolynomial.eval₂_X map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.prod_congr MvPolynomial.eval₂_sub RingHom.map_det Localization.isLocalization projVandermonde_map
det_vandermonde 📖	mathematical	—	det Fin.fintype vandermonde Finset.prod CommRing.toCommMonoid Finset.univ Finset.Ioi PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderTop SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	det.congr_simp vandermonde_eq_projVandermonde det_projVandermonde Finset.prod_congr mul_one
det_vandermonde_add 📖	mathematical	—	det Fin.fintype vandermonde Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	det_vandermonde Finset.prod_congr add_sub_add_right_eq_sub
det_vandermonde_eq_zero_iff 📖	mathematical	—	det Fin.fintype vandermonde MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	det_vandermonde IsDomain.toNontrivial IsDomain.to_noZeroDivisors LT.lt.ne' Finset.mem_Ioi det_zero_of_row_eq vandermonde_apply
det_vandermonde_id_eq_superFactorial 📖	mathematical	—	det Fin.fintype vandermonde AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.superFactorial	—	det.congr_simp Nat.cast_zero det_unique pow_zero Nat.cast_one Nat.superFactorial.eq_2 det_vandermonde Fin.prod_univ_succAbove Nat.cast_mul Finset.prod_congr sub_zero Finset.prod_natCast Fin.Ioi_zero_eq_map Finset.prod_map Fin.prod_univ_eq_prod_range Finset.prod_range_add_one_eq_factorial Nat.cast_add Fin.prod_Ioi_succ add_sub_add_right_eq_sub
det_vandermonde_ne_zero_iff 📖	—	—	—	—	—
det_vandermonde_sub 📖	mathematical	—	det Fin.fintype vandermonde SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	det_vandermonde_add det.congr_simp
eq_zero_of_forall_index_sum_mul_pow_eq_zero 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Pi.instZero	—	eq_zero_of_forall_index_sum_pow_mul_eq_zero Finset.sum_congr mul_comm
eq_zero_of_forall_index_sum_pow_mul_eq_zero 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Pi.instZero	—	eq_zero_of_mulVec_eq_zero det_vandermonde_ne_zero_iff
eq_zero_of_forall_pow_sum_mul_pow_eq_zero 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Pi.instZero	—	eq_zero_of_vecMul_eq_zero det_vandermonde_ne_zero_iff
eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials 📖	mathematical	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike of Polynomial.eval instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid vandermonde Polynomial.coeff	—	ext Finset.sum_congr Polynomial.eval₂_def Polynomial.supp_subset_range Fin.prop Polynomial.sum_eq_of_subset MulZeroClass.zero_mul Fin.sum_univ_eq_sum_range mul_comm of_apply RingHom.id_apply
projVandermonde_apply 📖	mathematical	—	projVandermonde Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
projVandermonde_apply_of_ne_zero 📖	mathematical	—	projVandermonde EuclideanDomain.toCommRing Field.toEuclideanDomain DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	projVandermonde_apply eq_div_iff isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain EuclideanDomain.toNontrivial mul_assoc pow_add Fin.rev_add_cast
projVandermonde_apply_zero_right 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	projVandermonde Pi.single Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	LE.le.eq_or_lt pow_zero mul_one Pi.single_eq_same projVandermonde_apply Pi.single_eq_of_ne LT.lt.ne zero_pow MulZeroClass.mul_zero
projVandermonde_comp 📖	mathematical	—	projVandermonde submatrix	—	—
projVandermonde_map 📖	mathematical	—	projVandermonde DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Matrix nonAssocSemiring Fin.fintype RingHom.mapMatrix	—	ext map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
rectVandermonde_apply 📖	mathematical	—	rectVandermonde Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
rectVandermonde_apply_zero_right 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	rectVandermonde Pi.single Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	LE.le.eq_or_lt pow_zero mul_one Pi.single_eq_same rectVandermonde_apply Pi.single_eq_of_ne LT.lt.ne zero_pow MulZeroClass.mul_zero
superFactorial_dvd_vandermonde_det 📖	mathematical	—	Nat.superFactorial det Fin.fintype Int.instCommRing vandermonde	—	Finset.mem_univ Finset.inf'_le det_eval_matrixOfPolynomials_eq_det_vandermonde descPochhammer_natDegree IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Int.instNontrivial monic_descPochhammer det.congr_simp det_vandermonde_sub Fin.prod_univ_eq_prod_range Nat.prod_range_succ_factorial
vandermonde_apply 📖	mathematical	—	vandermonde Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
vandermonde_cons 📖	mathematical	—	vandermonde Fin.cons Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	ext Fin.cons_zero Fin.cons_succ pow_zero pow_succ'
vandermonde_eq_projVandermonde 📖	mathematical	—	vandermonde projVandermonde Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	one_pow mul_one
vandermonde_mul_vandermonde_transpose 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid vandermonde transpose Finset.sum Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	Finset.sum_congr mul_pow
vandermonde_succ 📖	mathematical	—	vandermonde DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike of Fin.cons Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Fin.tail	—	Fin.cons_self_tail vandermonde_cons
vandermonde_transpose_mul_vandermonde 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transpose vandermonde Finset.sum Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	Finset.sum_congr pow_add

---

← Back to Index