Documentation Verification Report

IsConjRoot

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

Statistics

Metric	Count
Definitions `IsConjRoot`, `decidable`, `setoid`	3
Theorems `add_algebraMap`, `aeval_eq_zero`, `comm`, `eq_algebraMap`, `eq_algebraMap_of_injective`, `eq_zero`, `eq_zero_of_injective`, `exists_algEquiv`, `instIsEquiv`, `isIntegral`, `isIntegral_iff`, `ne_zero`, `ne_zero_of_injective`, `neg`, `of_isScalarTower`, `refl`, `sub_algebraMap`, `trans`, `isConjRoot_algHom_iff`, `isConjRoot_algHom_iff_of_injective`, `isConjRoot_def`, `isConjRoot_iff_aeval_eq_zero`, `isConjRoot_iff_eq_algebraMap`, `isConjRoot_iff_eq_algebraMap'`, `isConjRoot_iff_eq_algebraMap_of_injective`, `isConjRoot_iff_exists_algEquiv`, `isConjRoot_iff_mem_minpoly_aroots`, `isConjRoot_iff_mem_minpoly_rootSet`, `isConjRoot_iff_orbitRel`, `isConjRoot_of_aeval_eq_zero`, `isConjRoot_of_algEquiv`, `isConjRoot_of_algEquiv'`, `isConjRoot_of_algEquiv₂`, `isConjRoot_zero_iff_eq_zero`, `isConjRoot_zero_iff_eq_zero'`, `isConjRoot_zero_iff_eq_zero_of_injective`, `notMem_iff_exists_ne_and_isConjRoot`	37
Total	40

IsConjRoot

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	—
`setoid` 📖	CompOp	1 math math: `ConjRootClass.mk_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_algebraMap` 📖	mathematical	`IsConjRoot` `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`	—	`isConjRoot_def` `minpoly.add_algebraMap`
`aeval_eq_zero` 📖	mathematical	`IsConjRoot`	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `minpoly` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`minpoly.aeval`
`comm` 📖	mathematical	—	`IsConjRoot`	—	`symm`
`eq_algebraMap` 📖	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	—	`eq_algebraMap_of_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial`
`eq_algebraMap_of_injective` 📖	—	`IsConjRoot` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	—	`Polynomial.mem_aroots` `IsDomain.toNontrivial` `minpoly.aeval` `eq_1` `Polynomial.aroots_X_sub_C`
`eq_zero` 📖	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—	`eq_zero_of_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial`
`eq_zero_of_injective` 📖	—	`IsConjRoot` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	—	`eq_algebraMap_of_injective` `RingHom.map_zero`
`exists_algEquiv` 📖	mathematical	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike`	—	`IntermediateField.exists_algHom_of_splits_of_aeval` `normal_iff` `minpoly.aeval` `AlgHom.normal_bijective` `IsScalarTower.right`
`instIsEquiv` 📖	mathematical	—	`IsEquiv` `IsConjRoot`	—	`Quotient.instIsEquivEquiv`
`isIntegral` 📖	—	`IsIntegral` `IsConjRoot`	—	—	`minpoly.monic` `minpoly.aeval`
`isIntegral_iff` 📖	mathematical	`IsConjRoot`	`IsIntegral`	—	`isIntegral` `symm`
`ne_zero` 📖	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing`	—	—	`ne_zero_of_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial`
`ne_zero_of_injective` 📖	—	`IsConjRoot` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	—	`eq_zero_of_injective` `symm`
`neg` 📖	mathematical	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`isConjRoot_def` `minpoly.neg`
`of_isScalarTower` 📖	—	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `IsConjRoot`	—	—	`isConjRoot_of_aeval_eq_zero` `minpoly.aeval_of_isScalarTower` `aeval_eq_zero`
`refl` 📖	mathematical	—	`IsConjRoot`	—	—
`sub_algebraMap` 📖	mathematical	`IsConjRoot` `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`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `add_algebraMap`
`trans` 📖	—	`IsConjRoot`	—	—	—

(root)

Definitions

Name	Category	Theorems
`IsConjRoot` 📖	MathDef	23 math math: `IsConjRoot.instIsEquiv`, `isConjRoot_iff_mem_minpoly_aroots`, `isConjRoot_of_algEquiv`, `isConjRoot_iff_exists_algEquiv`, `isConjRoot_algHom_iff`, `isConjRoot_def`, `isConjRoot_of_algEquiv₂`, `isConjRoot_iff_aeval_eq_zero`, `isConjRoot_zero_iff_eq_zero_of_injective`, `isConjRoot_iff_eq_algebraMap_of_injective`, `isConjRoot_iff_eq_algebraMap`, `isConjRoot_iff_mem_minpoly_rootSet`, `isConjRoot_of_aeval_eq_zero`, `isConjRoot_of_algEquiv'`, `isConjRoot_algHom_iff_of_injective`, `isConjRoot_zero_iff_eq_zero`, `isConjRoot_zero_iff_eq_zero'`, `isConjRoot_iff_orbitRel`, `IsConjRoot.refl`, `IsConjRoot.comm`, `ConjRootClass.mk_eq_mk`, `notMem_iff_exists_ne_and_isConjRoot`, `isConjRoot_iff_eq_algebraMap'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConjRoot_algHom_iff` 📖	mathematical	—	`IsConjRoot` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Ring.toSemiring` `AlgHom.funLike` `DivisionRing.toRing`	—	`isConjRoot_algHom_iff_of_injective` `RingHom.injective` `DivisionRing.isSimpleRing`
`isConjRoot_algHom_iff_of_injective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgHom.funLike`	`IsConjRoot`	—	`isConjRoot_def` `minpoly.algHom_eq`
`isConjRoot_def` 📖	mathematical	—	`IsConjRoot` `minpoly`	—	—
`isConjRoot_iff_aeval_eq_zero` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsConjRoot` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `minpoly` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`IsConjRoot.aeval_eq_zero` `isConjRoot_of_aeval_eq_zero`
`isConjRoot_iff_eq_algebraMap` 📖	mathematical	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`isConjRoot_iff_eq_algebraMap_of_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial`
`isConjRoot_iff_eq_algebraMap'` 📖	mathematical	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`isConjRoot_iff_eq_algebraMap_of_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial`
`isConjRoot_iff_eq_algebraMap_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`IsConjRoot` `CommRing.toRing`	—	`IsConjRoot.eq_algebraMap_of_injective`
`isConjRoot_iff_exists_algEquiv` 📖	mathematical	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike`	—	`IsConjRoot.exists_algEquiv` `IsConjRoot.symm` `isConjRoot_of_algEquiv`
`isConjRoot_iff_mem_minpoly_aroots` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing`	`IsConjRoot` `Multiset` `Multiset.instMembership` `Polynomial.aroots` `minpoly`	—	`Polynomial.mem_aroots` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isConjRoot_iff_aeval_eq_zero` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`isConjRoot_iff_mem_minpoly_rootSet` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing`	`IsConjRoot` `Set` `Set.instMembership` `Polynomial.rootSet` `minpoly`	—	`isConjRoot_iff_mem_minpoly_aroots` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial` `Polynomial.eval_map_algebraMap`
`isConjRoot_iff_orbitRel` 📖	mathematical	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `MulAction.orbitRel` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulSemiringAction.toDistribMulAction` `AlgEquiv.applyMulSemiringAction`	—	`isConjRoot_iff_exists_algEquiv`
`isConjRoot_of_aeval_eq_zero` 📖	mathematical	`IsIntegral` `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` `minpoly` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`IsConjRoot`	—	`minpoly.eq_of_irreducible_of_monic` `IsDomain.toNontrivial` `minpoly.irreducible` `instIsDomain` `minpoly.monic`
`isConjRoot_of_algEquiv` 📖	mathematical	—	`IsConjRoot` `DFunLike.coe` `AlgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgEquiv.instFunLike`	—	`minpoly.algEquiv_eq`
`isConjRoot_of_algEquiv'` 📖	mathematical	—	`IsConjRoot` `DFunLike.coe` `AlgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgEquiv.instFunLike`	—	`minpoly.algEquiv_eq`
`isConjRoot_of_algEquiv₂` 📖	mathematical	—	`IsConjRoot` `DFunLike.coe` `AlgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `AlgEquiv.instFunLike`	—	`isConjRoot_def` `minpoly.algEquiv_eq`
`isConjRoot_zero_iff_eq_zero` 📖	mathematical	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`isConjRoot_zero_iff_eq_zero_of_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial`
`isConjRoot_zero_iff_eq_zero'` 📖	mathematical	—	`IsConjRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`isConjRoot_zero_iff_eq_zero_of_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial`
`isConjRoot_zero_iff_eq_zero_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`IsConjRoot` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`IsConjRoot.eq_zero_of_injective`
`notMem_iff_exists_ne_and_isConjRoot` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly`	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `IsConjRoot`	—	`instIsDomain` `minpoly.two_le_natDegree_iff` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsSeparable.isIntegral` `Polynomial.card_rootSet_eq_natDegree` `Fintype.one_lt_card_iff_nontrivial` `Polynomial.mem_rootSet` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `minpoly.ne_zero` `minpoly.aeval` `nontrivial_iff_exists_ne` `Subtype.coe_ne_coe` `isConjRoot_iff_mem_minpoly_rootSet`

---

← Back to Index