Radical

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

Statistics

Metric	Count
Definitions	0
Theorems degree_radical_le, divRadical_dvd_derivative, divRadical_dvd_wronskian_left, divRadical_dvd_wronskian_right, natDegree_radical_le	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degree_radical_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield UniqueFactorizationMonoid.radical Polynomial CommSemiring.toCommMonoidWithZero Polynomial.commSemiring Semifield.toCommSemiring Polynomial.instNormalizationMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.commRing Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain	—	Polynomial.degree_le_of_dvd IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain UniqueFactorizationMonoid.radical_dvd_self
divRadical_dvd_derivative 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain EuclideanDomain.divRadical Polynomial.instEuclideanDomain Polynomial.instNormalizationMonoid IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing EuclideanDomain.to_principal_ideal_domain DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative	—	UniqueFactorizationMonoid.induction_on_coprime PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain IsDomain.to_noZeroDivisors Polynomial.derivative_zero dvd_zero IsUnit.dvd EuclideanDomain.divRadical_isUnit pow_zero Polynomial.derivative_one mul_dvd_mul_iff_left Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero UniqueFactorizationMonoid.radical_ne_zero Polynomial.nontrivial EuclideanDomain.toNontrivial EuclideanDomain.radical_mul_divRadical UniqueFactorizationMonoid.radical_pow_of_prime Polynomial.derivative_pow_succ mul_assoc dvd_mul_of_dvd_left mul_comm dvd_mul_of_dvd_right pow_succ pow_ne_zero isReduced_of_noZeroDivisors Polynomial.instNoZeroDivisors Prime.ne_zero dvd_normalize_iff dvd_refl EuclideanDomain.isCoprime_of_dvd not_isUnit_zero zero_dvd_iff EuclideanDomain.divRadical_mul Polynomial.derivative_mul dvd_add Distrib.leftDistribClass mul_dvd_mul EuclideanDomain.divRadical_dvd_self
divRadical_dvd_wronskian_left 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain EuclideanDomain.divRadical Polynomial.instEuclideanDomain Polynomial.instNormalizationMonoid IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing EuclideanDomain.to_principal_ideal_domain Polynomial.wronskian	—	IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain Polynomial.wronskian.eq_1 dvd_sub dvd_mul_of_dvd_left EuclideanDomain.divRadical_dvd_self divRadical_dvd_derivative
divRadical_dvd_wronskian_right 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain EuclideanDomain.divRadical Polynomial.instEuclideanDomain Polynomial.instNormalizationMonoid IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing EuclideanDomain.to_principal_ideal_domain Polynomial.wronskian	—	IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain Polynomial.wronskian_neg_eq dvd_neg divRadical_dvd_wronskian_left
natDegree_radical_le 📖	mathematical	—	Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield UniqueFactorizationMonoid.radical Polynomial CommSemiring.toCommMonoidWithZero Polynomial.commSemiring Semifield.toCommSemiring Polynomial.instNormalizationMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.commRing Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain	—	IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain UniqueFactorizationMonoid.radical.congr_simp UniqueFactorizationMonoid.radical_zero Polynomial.natDegree_one Polynomial.natDegree_le_of_dvd UniqueFactorizationMonoid.radical_dvd_self

---

← Back to Index