Documentation Verification Report

RationalRoot

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

Statistics

Metric	Count
Definitions	0
Theorems `instIsIntegrallyClosed`, `integer_of_integral`, `den_dvd_of_is_root`, `exists_integer_of_is_root_of_monic`, `isInteger_of_is_root_of_monic`, `num_dvd_of_is_root`, `num_isRoot_scaleRoots_of_aeval_eq_zero`, `scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero`	8
Total	8

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIntegrallyClosed` 📖	mathematical	—	`IsIntegrallyClosed`	—	`isIntegrallyClosed_iff` `Localization.isLocalization` `integer_of_integral`
`integer_of_integral` 📖	mathematical	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing`	`IsLocalization.IsInteger` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield`	—	`isInteger_of_is_root_of_monic`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`den_dvd_of_is_root` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `IsFractionRing.den` `Polynomial.leadingCoeff`	—	`Polynomial.coeff_scaleRoots_natDegree` `Polynomial.dvd_term_of_isRoot_of_dvd_terms` `num_isRoot_scaleRoots_of_aeval_eq_zero` `Polynomial.coeff_scaleRoots` `Dvd.dvd.mul_right` `dvd_mul_of_dvd_right` `pow_one` `pow_dvd_pow` `lt_tsub_iff_left` `Nat.instOrderedSub` `add_zero` `Polynomial.coeff_eq_zero_of_natDegree_lt` `lt_of_le_of_ne` `Polynomial.natDegree_scaleRoots` `MulZeroClass.zero_mul` `dvd_zero` `UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `Prime.not_unit` `IsFractionRing.num_den_reduced` `Prime.dvd_of_dvd_pow`
`exists_integer_of_is_root_of_monic` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `Polynomial.coeff`	—	`den_dvd_of_is_root` `IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors` `IsDomain.toNontrivial` `Subtype.prop` `IsFractionRing.mk'_num_den'` `div_eq_iff` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_assoc` `mul_comm` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `mul_one` `mul_dvd_mul` `num_dvd_of_is_root`
`isInteger_of_is_root_of_monic` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsLocalization.IsInteger` `Semifield.toCommSemiring`	—	`IsFractionRing.isInteger_of_isUnit_den` `isUnit_of_dvd_one` `den_dvd_of_is_root`
`num_dvd_of_is_root` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `IsFractionRing.num` `Polynomial.coeff`	—	`pow_zero` `mul_one` `Polynomial.dvd_term_of_isRoot_of_dvd_terms` `num_isRoot_scaleRoots_of_aeval_eq_zero` `dvd_mul_of_dvd_right` `pow_one` `pow_dvd_pow` `bot_lt_iff_ne_bot` `IsFractionRing.num.congr_simp` `IsFractionRing.num_zero` `IsDomain.to_noZeroDivisors` `isReduced_of_noZeroDivisors` `IsDomain.toNontrivial` `Polynomial.coeff_scaleRoots` `tsub_zero` `Nat.instOrderedSub` `UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors` `Prime.not_unit` `IsFractionRing.num_den_reduced` `Prime.dvd_of_dvd_pow`
`num_isRoot_scaleRoots_of_aeval_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Polynomial.IsRoot` `Polynomial.scaleRoots` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `IsFractionRing.den` `IsFractionRing.num`	—	`Polynomial.isRoot_of_eval₂_map_eq_zero` `IsFractionRing.injective` `scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero` `IsFractionRing.mk'_num_den`
`scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `IsLocalization.mk'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Polynomial.scaleRoots` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike`	—	`Polynomial.aeval_def` `IsLocalization.mk'_spec'` `Polynomial.scaleRoots_eval₂_eq_zero`

---

← Back to Index