Field

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

Statistics

Metric	Count
Definitions `fintype`, `subtypeProd`, `rootsOfMinPolyPiType`	3
Theorems `eq_minpoly`, `add_algebraMap`, `aeval_of_isScalarTower`, `aux_inj_roots_of_min_poly`, `coeff_zero_eq_zero`, `coeff_zero_ne_zero`, `degree_le_of_ne_zero`, `dvd`, `dvd_iff`, `dvd_map_of_isScalarTower`, `dvd_map_of_isScalarTower'`, `eq_X_sub_C`, `eq_X_sub_C'`, `eq_iff_aeval_eq_zero`, `eq_iff_aeval_minpoly_eq_zero`, `eq_of_irreducible`, `eq_of_irreducible_of_monic`, `isRadical`, `ker_aeval_eq_span_minpoly`, `map_algebraMap`, `map_eq_of_equiv_equiv`, `ne_zero_of_finite`, `neg`, `one`, `prime`, `root`, `sub_algebraMap`, `unique`, `unique_of_degree_le_degree_minpoly`, `zero`, `minpoly_algEquiv_toLinearMap`, `minpoly_algHom_toLinearMap`	32
Total	35

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minpoly_algEquiv_toLinearMap` 📖	mathematical	`IsOfFinOrder` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut`	`minpoly` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommRing.toCommSemiring` `Algebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.End.instRing` `Ring.toAddCommGroup` `CommRing.toRing` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.toLinearMap` `Polynomial` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toPow` `Polynomial.semiring` `Polynomial.X` `orderOf` `AlgEquiv` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`smulCommClass_self` `IsScalarTower.left` `minpoly.unique` `Polynomial.monic_X_pow_sub_C` `LT.lt.ne` `IsOfFinOrder.orderOf_pos` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Polynomial.aeval_sub` `map_pow` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `pow_orderOf_eq_one` `sub_self` `Polynomial.degree_eq_natDegree` `Polynomial.Monic.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.degree_X_pow_sub_C` `Nat.cast_le` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `not_lt` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Fintype.linearIndependent_iff` `LinearIndependent.comp` `linearIndependent_algHom_toLinearMap'` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `AlgEquiv.coe_algHom_injective` `Subtype.val_injective` `Equiv.injective` `Finset.sum_congr` `Fin.sum_univ_eq_sum_range` `Polynomial.aeval_eq_sum_range'`
`minpoly_algHom_toLinearMap` 📖	mathematical	`IsOfFinOrder` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AlgHom.End`	`minpoly` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommRing.toCommSemiring` `Algebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.End.instRing` `Ring.toAddCommGroup` `CommRing.toRing` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.toLinearMap` `Polynomial` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toPow` `Polynomial.semiring` `Polynomial.X` `orderOf` `AlgHom` `AlgHom.End` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MonoidHom.coe_coe` `orderOf_injective` `MulEquiv.injective` `orderOf_units` `IsOfFinOrder.val_unit` `smulCommClass_self` `IsScalarTower.left` `minpoly_algEquiv_toLinearMap` `orderOf_pos_iff` `LinearMap.ext`

minpoly

Definitions

Name	Category	Theorems
`rootsOfMinPolyPiType` 📖	CompOp	1 math math: `aux_inj_roots_of_min_poly`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_algebraMap` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Polynomial.comp` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `Polynomial.semiring` `Polynomial.C`	—	`unique` `Polynomial.Monic.comp_X_sub_C` `monic` `Polynomial.aeval_comp` `Polynomial.aeval_sub` `Polynomial.aeval_X` `Polynomial.aeval_C` `add_sub_cancel_right` `aeval` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `min` `Polynomial.Monic.comp_X_add_C` `Polynomial.degree_eq_natDegree` `Polynomial.Monic.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.natDegree_comp` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.natDegree_X_sub_C` `mul_one` `Polynomial.natDegree_X_add_C` `ne_zero` `eq_zero` `IsIntegral.sub` `isIntegral_algebraMap` `Polynomial.zero_comp`
`aeval_of_isScalarTower` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`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` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero` `dvd_map_of_isScalarTower` `Polynomial.aeval_map_algebraMap`
`aux_inj_roots_of_min_poly` 📖	mathematical	—	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `rootsOfMinPolyPiType`	—	`IsNoetherianRing.strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Module.Free.of_divisionRing` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `LinearMap.ext_on` `Module.Basis.span_eq` `DFunLike.ext'_iff`
`coeff_zero_eq_zero` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Polynomial.zero_isRoot_of_coeff_zero_eq_zero` `root` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero` `IsDomain.toNontrivial` `Polynomial.coeff_X_zero`
`coeff_zero_ne_zero` 📖	—	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—	`Mathlib.Tactic.Contrapose.contrapose₄`
`degree_le_of_ne_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`min` `Polynomial.monic_mul_leadingCoeff_inv` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_C` `MulZeroClass.zero_mul` `Polynomial.degree_mul_leadingCoeff_inv`
`dvd` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `minpoly`	—	`IsAlgebraic.isIntegral` `Polynomial.modByMonic_eq_zero_iff_dvd` `monic` `LE.le.not_gt` `degree_le_of_ne_zero` `Polynomial.aeval_modByMonic_eq_self_of_root` `aeval` `Polynomial.degree_modByMonic_lt` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`dvd_iff` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `minpoly` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `aeval` `MulZeroClass.zero_mul` `dvd`
`dvd_map_of_isScalarTower` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `minpoly` `Polynomial.map` `algebraMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`dvd` `Polynomial.aeval_map_algebraMap` `aeval`
`dvd_map_of_isScalarTower'` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `minpoly` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `Polynomial.map` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommRing.toRing`	—	`dvd` `Polynomial.map_aeval_eq_aeval_map` `IsScalarTower.algebraMap_eq` `aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`eq_X_sub_C` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `Polynomial.semiring` `Polynomial.C`	—	`RingHom.injective` `DivisionRing.isSimpleRing`
`eq_X_sub_C'` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.id` `CommRing.toCommSemiring` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Polynomial.instSub` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`eq_X_sub_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`eq_iff_aeval_eq_zero` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.Monic`	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`aeval` `eq_of_irreducible_of_monic`
`eq_iff_aeval_minpoly_eq_zero` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`eq_iff_aeval_eq_zero` `irreducible` `instIsDomain` `monic`
`eq_of_irreducible` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Polynomial.leadingCoeff` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Polynomial.leadingCoeff_ne_zero` `Irreducible.ne_zero` `eq_of_irreducible_of_monic` `Associated.irreducible` `Polynomial.C_mul` `inv_mul_cancel₀` `Polynomial.C_1` `mul_inv_cancel₀` `Polynomial.aeval_mul` `MulZeroClass.zero_mul` `Polynomial.Monic.eq_1` `Polynomial.leadingCoeff_mul` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.leadingCoeff_C`
`eq_of_irreducible_of_monic` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.Monic`	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`dvd` `Polynomial.eq_of_monic_of_associated` `monic` `Associated.mul_left` `associated_one_iff_isUnit` `Irreducible.isUnit_or_isUnit` `not_isUnit` `mul_one`
`isRadical` 📖	mathematical	—	`IsRadical` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `minpoly`	—	`dvd_iff` `IsReduced.eq_zero` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`ker_aeval_eq_span_minpoly` 📖	mathematical	—	`RingHom.ker` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AlgHom` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval` `Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `Semiring.toModule` `Set` `Set.instSingletonSet` `minpoly`	—	`Ideal.ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`map_algebraMap` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subsemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Polynomial.lifts` `algebraMap` `Semifield.toCommSemiring` `minpoly`	`Polynomial.map` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `algebraMap` `Semifield.toCommSemiring` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing`	—	`Polynomial.eq_of_monic_of_dvd_of_natDegree_le` `monic` `IsIntegral.tower_top` `Function.Injective.monic_map_iff` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `dvd` `Polynomial.aeval_map_algebraMap` `aeval` `Polynomial.lifts_and_natDegree_eq_and_monic` `Polynomial.natDegree_map` `Polynomial.natDegree_le_of_dvd` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsScalarTower.right` `IsScalarTower.algebraMap_eq` `Polynomial.coe_mapRingHom` `Polynomial.mapRingHom_comp` `RingHom.comp_apply` `Polynomial.Monic.ne_zero`
`map_eq_of_equiv_equiv` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `algebraMap` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Semiring.toNonAssocSemiring` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `minpoly` `DFunLike.coe` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `eq_of_irreducible_of_monic` `IsDomain.toNontrivial` `Polynomial.mapEquiv_apply` `MulEquiv.irreducible_iff` `RingEquivClass.toMulEquivClass` `irreducible` `Algebra.IsIntegral.isIntegral` `aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Polynomial.map_aeval_eq_aeval_map` `Polynomial.Monic.map` `monic`
`ne_zero_of_finite` 📖	—	—	—	—	`ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsIntegral.of_finite`
`neg` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instMul` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instNeg` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.instOne` `Polynomial.natDegree` `Polynomial.comp` `Polynomial.X`	—	`unique` `Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X` `monic` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Polynomial.aeval_neg` `map_one` `MonoidHomClass.toOneHomClass` `Polynomial.aeval_comp` `Polynomial.aeval_X` `neg_neg` `aeval` `MulZeroClass.mul_zero` `min` `Polynomial.degree_mul` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.degree_pow` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.degree_neg` `Polynomial.degree_one` `nsmul_zero` `Polynomial.degree_comp_neg_X` `zero_add` `eq_zero` `Iff.not` `IsIntegral.neg_iff` `Polynomial.zero_comp` `pow_zero`
`one` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `Polynomial.instOne`	—	`sub_eq_add_neg` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `eq_X_sub_C`
`prime` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Prime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toCommMonoidWithZero` `Polynomial.commSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `minpoly`	—	`ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `not_isUnit` `IsDomain.toNontrivial` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `aeval` `MulZeroClass.zero_mul` `IsDomain.to_noZeroDivisors` `dvd`
`root` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.IsRoot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpoly`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Polynomial.eq_of_monic_of_associated` `monic` `Polynomial.monic_X_sub_C` `associated_of_dvd_dvd` `Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `Irreducible.dvd_symm` `Polynomial.irreducible_X_sub_C` `irreducible` `Polynomial.dvd_iff_isRoot` `aeval` `sub_eq_zero` `Polynomial.aeval_C` `Polynomial.aeval_X` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`
`sub_algebraMap` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Polynomial.comp` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.instAdd` `Polynomial.X` `Polynomial.semiring` `Polynomial.C`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `neg_neg` `add_algebraMap`
`unique` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree`	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`eq_of_sub_eq_zero` `LE.le.not_gt` `degree_le_of_ne_zero` `Polynomial.aeval_sub` `aeval` `sub_self` `Polynomial.degree_sub_lt` `le_antisymm` `min` `monic` `ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.Monic.leadingCoeff`
`unique_of_degree_le_degree_minpoly` 📖	mathematical	`Polynomial.Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly`	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`unique` `LE.le.trans` `min`
`zero` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.X` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `sub_eq_add_neg` `neg_zero` `add_zero` `eq_X_sub_C`

minpoly.AlgHom

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	11 math math: `sum_smul_minpolyDiv_eq_X_pow`, `finrank_algHom`, `Algebra.norm_eq_prod_embeddings`, `Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans`, `sum_embeddings_eq_finrank_mul`, `AlgHom.card`, `AlgHom.card_le`, `trace_eq_sum_embeddings`, `AlgHom.card_of_splits`, `Algebra.prod_embeddings_eq_finrank_pow`, `FiniteField.card_algHom_of_finrank_dvd`

minpoly.Fintype

Definitions

Name	Category	Theorems
`subtypeProd` 📖	CompOp	—

minpoly.Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_minpoly` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.leadingCoeff` `minpoly`	—	`minpoly.eq_of_irreducible` `mul_comm` `mul_assoc` `Polynomial.C_mul` `inv_mul_cancel₀` `Polynomial.leadingCoeff_ne_zero` `Irreducible.ne_zero` `Polynomial.C_1` `mul_one`

---

← Back to Index