Documentation Verification Report

MinpolyDiv

📁 Source: Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Statistics

Metric	Count
Definitions `minpolyDiv`	1
Theorems `coeff_minpolyDiv`, `coeff_minpolyDiv_mem_adjoin`, `coeff_minpolyDiv_sub_pow_mem_span`, `eval_minpolyDiv_of_aeval_eq_zero`, `eval_minpolyDiv_self`, `eval₂_minpolyDiv_of_eval₂_eq_zero`, `eval₂_minpolyDiv_self`, `minpolyDiv_eq_of_isIntegrallyClosed`, `minpolyDiv_eq_zero`, `minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero`, `minpolyDiv_monic`, `minpolyDiv_ne_zero`, `minpolyDiv_spec`, `natDegree_minpolyDiv`, `natDegree_minpolyDiv_lt`, `natDegree_minpolyDiv_succ`, `span_coeff_minpolyDiv`, `sum_smul_minpolyDiv_eq_X_pow`	18
Total	19

(root)

Definitions

Name	Category	Theorems
`minpolyDiv` 📖	CompOp	17 math math: `eval_minpolyDiv_self`, `eval₂_minpolyDiv_self`, `eval₂_minpolyDiv_of_eval₂_eq_zero`, `natDegree_minpolyDiv_succ`, `sum_smul_minpolyDiv_eq_X_pow`, `eval_minpolyDiv_of_aeval_eq_zero`, `minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero`, `span_coeff_minpolyDiv`, `natDegree_minpolyDiv_lt`, `coeff_minpolyDiv_mem_adjoin`, `coeff_minpolyDiv`, `minpolyDiv_eq_of_isIntegrallyClosed`, `minpolyDiv_spec`, `minpolyDiv_eq_zero`, `Module.Basis.traceDual_powerBasis_eq`, `minpolyDiv_monic`, `natDegree_minpolyDiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_minpolyDiv` 📖	mathematical	—	`Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpolyDiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `minpoly` `CommRing.toRing` `Distrib.toMul`	—	`Polynomial.coeff_map` `minpolyDiv_spec` `mul_sub` `Polynomial.coeff_sub` `Polynomial.coeff_mul_X` `Polynomial.coeff_mul_C` `sub_add_cancel`
`coeff_minpolyDiv_mem_adjoin` 📖	mathematical	—	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Polynomial.coeff` `minpolyDiv`	—	`coeff_minpolyDiv` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Subalgebra.algebraMap_mem` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `Algebra.self_mem_adjoin_singleton` `Polynomial.coeff_eq_zero_of_natDegree_lt` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass`
`coeff_minpolyDiv_sub_pow_mem_span` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpolyDiv`	`Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Set.Iio` `Nat.instPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Polynomial.coeff`	—	`IsMin.Iio_eq` `Set.image_empty` `Submodule.span_empty` `tsub_zero` `Nat.instOrderedSub` `Polynomial.Monic.leadingCoeff` `minpolyDiv_monic` `pow_zero` `sub_self` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `coeff_minpolyDiv` `add_sub_assoc` `pow_succ` `sub_mul` `Algebra.algebraMap_eq_smul_one` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `Submodule.smul_mem` `Submodule.subset_span` `tsub_tsub` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_tsub_of_add_le_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsScalarTower.right` `SetLike.le_def` `instIsConcreteLE` `Submodule.span_mul_span` `Set.mul_singleton` `Set.image_image` `Submodule.span_mono` `Set.mem_Iio` `Submodule.mul_mem_mul` `LE.le.trans` `Submodule.mem_span_singleton_self`
`eval_minpolyDiv_of_aeval_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `minpoly` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Polynomial.eval` `minpolyDiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative`	—	`Polynomial.eval.eq_1` `eval₂_minpolyDiv_of_eval₂_eq_zero` `RingHomCompTriple.comp_eq` `RingHomCompTriple.right_ids` `RingHom.id_apply`
`eval_minpolyDiv_self` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpolyDiv` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `minpoly` `CommRing.toRing`	—	`Polynomial.eval_map_algebraMap` `Polynomial.derivative_map` `minpolyDiv_spec` `Polynomial.derivative_mul` `Polynomial.derivative_sub` `Polynomial.derivative_X` `Polynomial.derivative_C` `sub_zero` `mul_one` `Polynomial.eval_add` `Polynomial.eval_mul` `Polynomial.eval_sub` `Polynomial.eval_X` `Polynomial.eval_C` `sub_self` `MulZeroClass.mul_zero` `zero_add`
`eval₂_minpolyDiv_of_eval₂_eq_zero` 📖	mathematical	`Polynomial.eval₂` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.comp` `Semiring.toNonAssocSemiring` `algebraMap` `minpoly` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`minpolyDiv` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative`	—	`Polynomial.eval₂_hom` `eval_minpolyDiv_self` `Polynomial.eval₂_mul` `Polynomial.eval₂_sub` `Polynomial.eval₂_X` `Polynomial.eval₂_C` `IsDomain.to_noZeroDivisors` `minpolyDiv_spec` `Polynomial.eval₂_map`
`eval₂_minpolyDiv_self` 📖	mathematical	—	`Polynomial.eval₂` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `DFunLike.coe` `minpolyDiv` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Polynomial.aeval` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `minpoly` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`eval₂_minpolyDiv_of_eval₂_eq_zero` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `Polynomial.eval₂_map` `RingHom.coe_coe` `Polynomial.eval₂_hom` `Polynomial.eval_map_algebraMap` `minpoly.aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`minpolyDiv_eq_of_isIntegrallyClosed` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`minpolyDiv` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`IsScalarTower.algebraMap_eq` `Polynomial.map_map` `minpoly.isIntegrallyClosed_eq_field_fractions'`
`minpolyDiv_eq_zero` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`minpolyDiv` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instZero`	—	`Polynomial.map_zero` `Polynomial.zero_divByMonic`
`minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `minpoly` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Polynomial.eval` `minpolyDiv`	—	`Polynomial.eval_mul` `Polynomial.eval_sub` `Polynomial.eval_X` `Polynomial.eval_C` `IsDomain.to_noZeroDivisors` `minpolyDiv_spec` `Polynomial.eval_map_algebraMap` `sub_eq_zero`
`minpolyDiv_monic` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpolyDiv`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `minpolyDiv_spec` `Polynomial.leadingCoeff_X_sub_C` `mul_one` `Polynomial.Monic.leadingCoeff` `Polynomial.Monic.map` `minpoly.monic` `Polynomial.leadingCoeff_mul'` `minpolyDiv_ne_zero`
`minpolyDiv_ne_zero` 📖	—	`IsIntegral` `CommRing.toRing`	—	—	`minpolyDiv_spec` `Polynomial.Monic.ne_zero` `Polynomial.Monic.map` `minpoly.monic` `MulZeroClass.zero_mul`
`minpolyDiv_spec` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instMul` `minpolyDiv` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.map` `algebraMap` `minpoly`	—	`mul_comm` `Polynomial.mul_divByMonic_eq_iff_isRoot` `Polynomial.IsRoot.eq_1` `Polynomial.eval_map_algebraMap` `minpoly.aeval`
`natDegree_minpolyDiv` 📖	mathematical	—	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpolyDiv` `minpoly` `CommRing.toRing`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Polynomial.natDegree_of_subsingleton` `minpoly.subsingleton` `Polynomial.natDegree_one` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `natDegree_minpolyDiv_succ` `minpolyDiv_eq_zero` `minpoly.eq_zero`
`natDegree_minpolyDiv_lt` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpolyDiv` `minpoly`	—	`natDegree_minpolyDiv_succ`
`natDegree_minpolyDiv_succ` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpolyDiv` `minpoly`	—	`Polynomial.Monic.natDegree_map` `minpoly.monic` `minpolyDiv_spec` `Polynomial.natDegree_mul'` `Polynomial.leadingCoeff_X_sub_C` `mul_one` `minpolyDiv_ne_zero` `Polynomial.natDegree_sub_C` `Polynomial.natDegree_X`
`span_coeff_minpolyDiv` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Set.range` `Polynomial.coeff` `minpolyDiv` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `Algebra.adjoin` `Set` `Set.instSingletonSet`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `le_antisymm` `Submodule.span_le` `coeff_minpolyDiv_mem_adjoin` `Submodule.span_range_natDegree_eq_adjoin` `minpoly.monic` `minpoly.aeval` `Finset.coe_image` `Finset.coe_range` `Submodule.subset_span` `Set.mem_range_self` `Set.mem_preimage` `SetLike.mem_coe` `Submodule.sub_mem_iff_right` `SetLike.le_def` `instIsConcreteLE` `Set.image_subset_iff` `lt_trans` `coeff_minpolyDiv_sub_pow_mem_span` `Set.mem_Iio` `natDegree_minpolyDiv_succ`
`sum_smul_minpolyDiv_eq_X_pow` 📖	mathematical	`Algebra.adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Set` `Set.instSingletonSet` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule`	`Finset.sum` `AlgHom` `Polynomial` `Polynomial.commRing` `Finset.univ` `minpoly.AlgHom.fintype` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHomClass.toRingHom` `AlgHom.funLike` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.toSMul` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DFunLike.coe` `Polynomial.aeval` `LinearMap` `RingHom.id` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `minpoly` `minpolyDiv` `Polynomial.X`	—	`instIsDomain` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `sub_eq_zero` `AlgHom.ext_of_adjoin_eq_top` `Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero` `Finset.sum_congr` `Polynomial.map_smul` `map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `Polynomial.eval_sub` `Polynomial.eval_finset_sum` `Polynomial.eval_smul` `IsScalarTower.right` `Polynomial.eval_map` `eval₂_minpolyDiv_self` `mul_ite` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `Polynomial.eval_X_pow` `div_mul_cancel₀` `map_eq_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.Separable.aeval_derivative_ne_zero` `Algebra.IsSeparable.isSeparable` `minpoly.aeval` `LE.le.trans_lt` `Polynomial.natDegree_sub_le` `max_lt` `Polynomial.natDegree_sum_le` `Finset.fold_congr` `AlgHom.card` `Module.finrank_pos` `commRing_strongRankCondition` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LE.le.trans` `Polynomial.natDegree_smul_le` `Polynomial.natDegree_map_le` `LT.lt.trans_le` `natDegree_minpolyDiv_lt` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsSeparable.isAlgebraic` `minpoly.natDegree_le` `Polynomial.natDegree_pow` `IsDomain.to_noZeroDivisors` `Polynomial.natDegree_X` `mul_one`

---

← Back to Index