Wronskian

📁 Source: Mathlib/RingTheory/Polynomial/Wronskian.lean

Statistics

Metric	Count
Definitions wronskian, wronskianBilin	2
Theorems wronskian_eq_zero_iff, degree_wronskian_lt_add, isAlt_wronskianBilin, natDegree_wronskian_lt_add, wronskianBilin_apply, wronskian_add_left, wronskian_add_right, wronskian_eq_of_sum_zero, wronskian_neg_eq, wronskian_neg_left, wronskian_neg_right, wronskian_self_eq_zero, wronskian_zero_left, wronskian_zero_right	14
Total	16

IsCoprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
wronskian_eq_zero_iff 📖	mathematical	IsCoprime Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring	Polynomial.wronskian Polynomial.instZero DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative	—	Polynomial.dvd_derivative_iff dvd_of_dvd_mul_right zero_add sub_eq_iff_eq_add Polynomial.wronskian.eq_1 dvd_mul_right dvd_of_dvd_mul_left symm dvd_mul_left MulZeroClass.mul_zero MulZeroClass.zero_mul sub_self

Polynomial

Definitions

Name	Category	Theorems
wronskian 📖	CompOp	15 math math: wronskian_self_eq_zero, wronskian_add_right, wronskian_neg_right, wronskian_eq_of_sum_zero, wronskian_neg_eq, wronskian_zero_left, wronskianBilin_apply, degree_wronskian_lt_add, divRadical_dvd_wronskian_right, wronskian_add_left, natDegree_wronskian_lt_add, IsCoprime.wronskian_eq_zero_iff, divRadical_dvd_wronskian_left, wronskian_neg_left, wronskian_zero_right
wronskianBilin 📖	CompOp	2 math math: isAlt_wronskianBilin, wronskianBilin_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degree_wronskian_lt_add 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring CommRing.toCommSemiring wronskian WithBot.add	—	degree_sub_le max_lt_iff lt_of_le_of_lt degree_mul_le WithBot.add_lt_add_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le degree_ne_bot degree_derivative_lt WithBot.add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add
isAlt_wronskianBilin 📖	mathematical	—	LinearMap.IsAlt Polynomial CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring wronskianBilin	—	wronskian_self_eq_zero
natDegree_wronskian_lt_add 📖	mathematical	—	natDegree CommSemiring.toSemiring CommRing.toCommSemiring wronskian	—	wronskian_zero_left wronskian_zero_right WithBot.coe_lt_coe WithBot.coe_add degree_eq_natDegree degree_wronskian_lt_add
wronskianBilin_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass Algebra.id wronskianBilin wronskian	—	smulCommClass Algebra.to_smulCommClass
wronskian_add_left 📖	mathematical	—	wronskian Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd	—	LinearMap.map_add₂ smulCommClass Algebra.to_smulCommClass
wronskian_add_right 📖	mathematical	—	wronskian Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd	—	LinearMap.map_add smulCommClass Algebra.to_smulCommClass
wronskian_eq_of_sum_zero 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd instZero	wronskian	—	LinearMap.IsAlt.eq_of_add_add_eq_zero isAlt_wronskianBilin AddCancelMonoid.toIsCancelAdd
wronskian_neg_eq 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instNeg CommRing.toRing wronskian	—	LinearMap.IsAlt.neg isAlt_wronskianBilin
wronskian_neg_left 📖	mathematical	—	wronskian Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instNeg CommRing.toRing	—	LinearMap.map_neg₂ smulCommClass Algebra.to_smulCommClass
wronskian_neg_right 📖	mathematical	—	wronskian Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instNeg CommRing.toRing	—	LinearMap.map_neg smulCommClass Algebra.to_smulCommClass
wronskian_self_eq_zero 📖	mathematical	—	wronskian Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero	—	wronskian.eq_1 mul_comm sub_self
wronskian_zero_left 📖	mathematical	—	wronskian Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero	—	smulCommClass Algebra.to_smulCommClass wronskianBilin_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
wronskian_zero_right 📖	mathematical	—	wronskian Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero	—	LinearMap.map_zero smulCommClass Algebra.to_smulCommClass

---

← Back to Index