Basic

📁 Source: Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Statistics

Metric	Count
Definitions `algHomEquivAlgHomOfSplits`, `algHomEquivAlgHomOfSplits`, `IsAlgClosure`, `equiv`, `equivOfAlgebraic`, `equivOfAlgebraic'`, `equivOfEquiv`, `equivOfEquivAux`	8
Theorems `algHomEquivAlgHomOfSplits_apply_apply`, `range_eval_eq_rootSet_minpoly`, `algHomEquivAlgHomOfSplits_apply`, `algHomEquivAlgHomOfSplits_apply_apply`, `algHomEquivAlgHomOfSplits_symm_apply`, `eq_bot_of_isAlgClosed_of_isAlgebraic`, `algebraMap_bijective_of_isIntegral`, `associated_iff_roots_eq_roots`, `card_aroots_eq_natDegree`, `card_aroots_eq_natDegree_of_isUnit_leadingCoeff`, `card_aroots_eq_natDegree_of_leadingCoeff_ne_zero`, `card_roots_eq_natDegree`, `card_roots_map_eq_natDegree_from_simpleRing`, `card_roots_map_eq_natDegree_of_injective`, `card_roots_map_eq_natDegree_of_isUnit_leadingCoeff`, `card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero`, `degree_eq_one_of_irreducible`, `dvd_iff_roots_le_roots`, `eval_surjective`, `exists_aeval_eq_zero`, `exists_aeval_eq_zero_of_injective`, `exists_eq_mul_self`, `exists_eval₂_eq_zero`, `exists_eval₂_eq_zero_of_injective`, `exists_pow_nat_eq`, `exists_root`, `instInfinite`, `instIsAlgClosure`, `nonempty_algEquiv_or_of_finrank_eq_two`, `of_exists_root`, `of_ringEquiv`, `perfectField`, `perfectRing`, `ringHom_bijective_of_isIntegral`, `roots_eq_zero_iff`, `roots_eq_zero_iff_degree_nonpos`, `roots_eq_zero_iff_natDegree_eq_zero`, `splits`, `splits_codomain`, `splits_domain`, `surjective_restrictDomain_of_isAlgebraic`, `equivOfEquiv_algebraMap`, `equivOfEquiv_comp_algebraMap`, `equivOfEquiv_symm_algebraMap`, `equivOfEquiv_symm_comp_algebraMap`, `isAlgClosed`, `isAlgebraic`, `normal`, `ofAlgebraic`, `of_splits`, `separable`, `isCoprime_iff_aeval_ne_zero_of_isAlgClosed`, `isRoot_of_isRoot_iff_dvd_derivative_mul`, `isAlgClosure_iff`	54
Total	62

Algebra.IsAlgebraic

Definitions

Name	Category	Theorems
`algHomEquivAlgHomOfSplits` 📖	CompOp	1 math math: `algHomEquivAlgHomOfSplits_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHomEquivAlgHomOfSplits_apply_apply` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `algHomEquivAlgHomOfSplits` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—
`range_eval_eq_rootSet_minpoly` 📖	mathematical	—	`Set.range` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DFunLike.coe` `AlgHom.funLike` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain`	—	`range_eval_eq_rootSet_minpoly_of_splits` `IsAlgClosed.splits`

IntermediateField

Definitions

Name	Category	Theorems
`algHomEquivAlgHomOfSplits` 📖	CompOp	3 math math: `algHomEquivAlgHomOfSplits_symm_apply`, `algHomEquivAlgHomOfSplits_apply_apply`, `algHomEquivAlgHomOfSplits_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHomEquivAlgHomOfSplits_apply` 📖	mathematical	`Polynomial.Splits` `IntermediateField` `SetLike.instMembership` `instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `algebra'` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `Equiv` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `algHomEquivAlgHomOfSplits` `AlgHom.comp` `val`	—	`IsScalarTower.left`
`algHomEquivAlgHomOfSplits_apply_apply` 📖	mathematical	`Polynomial.Splits` `IntermediateField` `SetLike.instMembership` `instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `algebra'` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `algHomEquivAlgHomOfSplits` `RingHom` `Semiring.toNonAssocSemiring` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `RingHom.instFunLike` `instAlgebraSubtypeMem`	—	`IsScalarTower.left`
`algHomEquivAlgHomOfSplits_symm_apply` 📖	mathematical	`Polynomial.Splits` `IntermediateField` `SetLike.instMembership` `instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `algebra'` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `Equiv` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `algHomEquivAlgHomOfSplits` `AlgHom.codRestrict` `toSubalgebra`	—	`IsScalarTower.left`
`eq_bot_of_isAlgClosed_of_isAlgebraic` 📖	mathematical	—	`Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `bot_unique` `IsAlgClosed.algebraMap_bijective_of_isIntegral` `instIsDomain` `Algebra.IsAlgebraic.isIntegral` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass`

IsAlgClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_bijective_of_isIntegral` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial` `minpoly.monic` `Algebra.IsIntegral.isIntegral` `degree_eq_one_of_irreducible` `minpoly.irreducible` `instIsDomain` `minpoly.aeval` `add_eq_zero_iff_eq_neg` `Polynomial.aeval_C` `Polynomial.aeval_X` `Polynomial.aeval_add` `one_mul` `Polynomial.C_1` `Polynomial.eq_X_add_C_of_degree_eq_one` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`associated_iff_roots_eq_roots` 📖	mathematical	—	`Associated` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain`	—	`instIsDomain` `Associated.roots_eq` `associated_of_dvd_dvd` `Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `dvd_iff_roots_le_roots` `le_of_eq`
`card_aroots_eq_natDegree` 📖	mathematical	—	`Multiset.card` `Polynomial.aroots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`card_roots_map_eq_natDegree_of_injective` `FaithfulSMul.algebraMap_injective`
`card_aroots_eq_natDegree_of_isUnit_leadingCoeff` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.leadingCoeff`	`Multiset.card` `Polynomial.aroots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial.natDegree`	—	`card_roots_map_eq_natDegree_of_isUnit_leadingCoeff`
`card_aroots_eq_natDegree_of_leadingCoeff_ne_zero` 📖	mathematical	—	`Multiset.card` `Polynomial.aroots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero`
`card_roots_eq_natDegree` 📖	mathematical	—	`Multiset.card` `Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`instIsDomain` `Polynomial.exists_prod_multiset_X_sub_C_mul` `roots_eq_zero_iff_natDegree_eq_zero` `add_zero`
`card_roots_map_eq_natDegree_from_simpleRing` 📖	mathematical	—	`Multiset.card` `Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial.map` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.natDegree`	—	`instIsDomain` `card_roots_eq_natDegree` `Polynomial.natDegree_map` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`card_roots_map_eq_natDegree_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike`	`Multiset.card` `Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Polynomial.map` `Polynomial.natDegree`	—	`instIsDomain` `card_roots_eq_natDegree` `Polynomial.natDegree_map_eq_of_injective`
`card_roots_map_eq_natDegree_of_isUnit_leadingCoeff` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.leadingCoeff`	`Multiset.card` `Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial.map` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.natDegree`	—	`instIsDomain` `card_roots_eq_natDegree` `Polynomial.natDegree_map_eq_of_isUnit_leadingCoeff` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero` 📖	mathematical	—	`Multiset.card` `Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial.map` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.natDegree`	—	`instIsDomain` `card_roots_eq_natDegree` `Polynomial.natDegree_map_of_leadingCoeff_ne_zero`
`degree_eq_one_of_irreducible` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`Polynomial.degree` `WithBot` `WithBot.one` `Nat.instOne`	—	`Polynomial.Splits.degree_eq_one_of_irreducible` `splits`
`dvd_iff_roots_le_roots` 📖	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` `Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `Polynomial.roots` `instIsDomain`	—	`Polynomial.Splits.dvd_iff_roots_le_roots` `splits`
`eval_surjective` 📖	mathematical	—	`Polynomial.eval` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Polynomial.Splits.exists_eval_eq_zero` `splits` `Polynomial.degree_sub_C` `Polynomial.natDegree_pos_iff_degree_pos` `LT.lt.ne'` `Polynomial.eval_sub` `Polynomial.eval_C`
`exists_aeval_eq_zero` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `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`	—	`exists_aeval_eq_zero_of_injective` `FaithfulSMul.algebraMap_injective`
`exists_aeval_eq_zero_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap`	`AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`exists_eval₂_eq_zero_of_injective`
`exists_eq_mul_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Nat.instAtLeastTwoHAddOfNat` `exists_pow_nat_eq` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `sq`
`exists_eval₂_eq_zero` 📖	mathematical	—	`Polynomial.eval₂` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`exists_eval₂_eq_zero_of_injective` `RingHom.injective` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`exists_eval₂_eq_zero_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike`	`Polynomial.eval₂` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`exists_root` `Polynomial.degree_map_eq_of_injective` `Polynomial.eval₂_eq_eval_map` `Polynomial.IsRoot.eq_1`
`exists_pow_nat_eq` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Polynomial.degree_X_pow_sub_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ne_of_gt` `WithBot.coe_lt_coe` `exists_root` `sub_eq_zero` `Polynomial.eval_sub` `Polynomial.eval_pow` `Polynomial.eval_X` `Polynomial.eval_C`
`exists_root` 📖	mathematical	—	`Polynomial.IsRoot` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Polynomial.Splits.exists_eval_eq_zero` `splits`
`instInfinite` 📖	mathematical	—	`Infinite`	—	`Infinite.of_not_fintype` `Polynomial.separable_X_pow_sub_C` `Nat.cast_add` `Nat.cast_card_eq_zero` `Nat.cast_one` `zero_add` `NeZero.one` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `one_ne_zero` `instIsDomain` `Polynomial.card_rootSet_eq_natDegree` `splits_domain` `Polynomial.C_1` `Polynomial.natDegree_X_pow_sub_C` `Fintype.card_le_of_injective` `Subtype.coe_injective`
`instIsAlgClosure` 📖	mathematical	—	`IsAlgClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.id` `CommRing.toCommSemiring` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `CommSemiring.toSemiring` `instIsDomain` `Field.toSemifield` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self`
`nonempty_algEquiv_or_of_finrank_eq_two` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	`AlgEquiv` `Algebra.id`	—	`instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Subalgebra.isSimpleOrder_of_finrank` `IsSimpleOrder.eq_bot_or_eq_top`
`of_exists_root` 📖	mathematical	`Polynomial.eval` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsAlgClosed`	—	`Polynomial.monic_mul_leadingCoeff_inv` `Irreducible.ne_zero` `Polynomial.irreducible_mul_leadingCoeff_inv` `Polynomial.eval_mul` `Polynomial.eval_C` `IsDomain.to_noZeroDivisors` `instIsDomain` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `UniqueFactorizationMonoid.factors_prod` `Polynomial.Splits.mul` `Polynomial.Splits.multisetProd` `UniqueFactorizationMonoid.irreducible_of_factor` `Polynomial.Splits.of_degree_eq_one` `Polynomial.degree_eq_one_of_irreducible_of_root` `IsUnit.splits` `Units.isUnit`
`of_ringEquiv` 📖	mathematical	—	`IsAlgClosed`	—	`of_exists_root` `Polynomial.degree_map` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ne_of_gt` `Polynomial.degree_pos_of_irreducible` `exists_root` `RingEquiv.injective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Polynomial.IsRoot.eq_1` `Polynomial.induction_on` `Polynomial.eval_C` `Polynomial.map_C` `Polynomial.eval_add` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `Polynomial.map_add` `Polynomial.eval_mul` `Polynomial.eval_pow` `Polynomial.eval_X` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingEquiv.symm_apply_apply` `Polynomial.map_mul` `Polynomial.map_pow` `Polynomial.map_X`
`perfectField` 📖	mathematical	—	`PerfectField`	—	`CharP.exists'` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `PerfectField.ofCharZero` `PerfectRing.toPerfectField` `expChar_prime` `perfectRing`
`perfectRing` 📖	mathematical	—	`PerfectRing` `Semifield.toCommSemiring` `Field.toSemifield` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`PerfectRing.ofSurjective` `expChar_prime` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `exists_pow_nat_eq` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `NeZero.of_gt'` `Nat.Prime.one_lt'`
`ringHom_bijective_of_isIntegral` 📖	mathematical	`RingHom.IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing`	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`algebraMap_bijective_of_isIntegral`
`roots_eq_zero_iff` 📖	mathematical	—	`Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Multiset` `Multiset.instZero` `DFunLike.coe` `RingHom` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.coeff`	—	`instIsDomain` `le_or_gt` `Polynomial.eq_C_of_degree_le_zero` `exists_root` `LT.lt.ne'` `Polynomial.mem_roots` `Polynomial.ne_zero_of_degree_gt` `Polynomial.roots_C`
`roots_eq_zero_iff_degree_nonpos` 📖	mathematical	—	`Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Multiset` `Multiset.instZero` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`instIsDomain` `roots_eq_zero_iff_natDegree_eq_zero` `Polynomial.natDegree_eq_zero_iff_degree_le_zero`
`roots_eq_zero_iff_natDegree_eq_zero` 📖	mathematical	—	`Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Multiset` `Multiset.instZero` `Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`instIsDomain` `roots_eq_zero_iff` `Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero`
`splits` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	—
`splits_codomain` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`splits`
`splits_domain` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map`	—	`Polynomial.Splits.map` `splits`
`surjective_restrictDomain_of_isAlgebraic` 📖	mathematical	—	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `CommSemiring.toSemiring` `AlgHom.restrictDomain`	—	`IntermediateField.exists_algHom_of_splits'` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `splits`

IsAlgClosure

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—
`equivOfAlgebraic` 📖	CompOp	—
`equivOfAlgebraic'` 📖	CompOp	—
`equivOfEquiv` 📖	CompOp	4 math math: `equivOfEquiv_comp_algebraMap`, `equivOfEquiv_symm_algebraMap`, `equivOfEquiv_symm_comp_algebraMap`, `equivOfEquiv_algebraMap`
`equivOfEquivAux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivOfEquiv_algebraMap` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivOfEquiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingHom.ext_iff` `equivOfEquiv_comp_algebraMap`
`equivOfEquiv_comp_algebraMap` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `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` `equivOfEquiv` `algebraMap`	—	—
`equivOfEquiv_symm_algebraMap` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equivOfEquiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap`	—	`RingEquiv.injective` `RingEquiv.apply_symm_apply` `equivOfEquiv_algebraMap`
`equivOfEquiv_symm_comp_algebraMap` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `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` `RingEquiv.symm` `equivOfEquiv` `algebraMap`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingHom.ext_iff` `equivOfEquiv_symm_algebraMap`
`isAlgClosed` 📖	mathematical	—	`IsAlgClosed`	—	—
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `DivisionRing.toRing` `Field.toDivisionRing`	—	—
`normal` 📖	mathematical	—	`Normal`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `isAlgebraic` `IsAlgClosed.splits` `isAlgClosed`
`ofAlgebraic` 📖	mathematical	—	`IsAlgClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instIsDomain` `Field.toSemifield` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `isAlgClosed` `Algebra.IsAlgebraic.trans` `IsDomain.to_noZeroDivisors` `isAlgebraic`
`of_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap`	`IsAlgClosure`	—	`IsAlgClosed.of_exists_root` `Irreducible.exists_dvd_monic_irreducible_of_isIntegral` `Polynomial.Splits.exists_eval_eq_zero` `Polynomial.Splits.of_dvd` `instIsDomain` `Polynomial.map_monic_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.degree_ne_of_natDegree_ne` `LT.lt.ne'` `Irreducible.natDegree_pos` `Algebra.IsIntegral.isAlgebraic` `IsDomain.toNontrivial`
`separable` 📖	mathematical	—	`Algebra.IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `Irreducible.separable` `minpoly.irreducible` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `isAlgebraic`

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_iff_aeval_ne_zero_of_isAlgClosed` 📖	mathematical	—	`IsCoprime` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `commSemiring` `Semifield.toCommSemiring`	—	`aeval_ne_zero_of_isCoprime` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isCoprime_of_dvd` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `Mathlib.Tactic.Contrapose.contrapose₃` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsAlgClosed.exists_root` `degree_map` `DivisionRing.isSimpleRing` `ne_of_lt` `degree_pos_of_ne_zero_of_nonunit` `not_and_or` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `MulZeroClass.zero_mul`
`isRoot_of_isRoot_iff_dvd_derivative_mul` 📖	mathematical	—	`IsRoot` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instMul` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative`	—	`eval_zero` `MulZeroClass.mul_zero` `eq_C_of_derivative_eq_zero` `IsAddTorsionFree.of_isCancelMulZero_charZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `derivative_C` `MulZeroClass.zero_mul` `mul_ne_zero` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `IsAlgClosed.dvd_iff_roots_le_roots` `Multiset.le_iff_count` `count_roots` `rootMultiplicity_mul` `rootMultiplicity_pos` `derivative_rootMultiplicity_of_root` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_rfl` `instIsEmptyFalse` `rootMultiplicity_eq_zero` `Nat.instCanonicallyOrderedAdd` `isRoot_of_isRoot_of_dvd_derivative_mul`

(root)

Definitions

Name	Category	Theorems
`IsAlgClosure` 📖	CompData	13 math math: `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`, `IsAlgClosure.of_exists_root`, `IsAlgClosure.of_exist_roots`, `IsAlgClosed.instIsAlgClosure`, `AlgebraicClosure.instIsAlgClosureOfIsAlgebraic`, `IsAlgClosure.of_splits`, `AlgebraicClosure.instIsAlgClosure`, `IsAlgClosure.ofAlgebraic`, `IsSepClosure.isAlgClosure_of_perfectField_top`, `algebraicClosure.isAlgClosure`, `isAlgClosure_iff`, `IsAlgClosed.isAlgClosure_of_transcendence_basis`, `IsSepClosure.isAlgClosure_of_perfectField`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAlgClosure_iff` 📖	mathematical	—	`IsAlgClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instIsDomain` `Field.toSemifield` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `IsAlgClosed` `Algebra.IsAlgebraic`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsAlgClosure.isAlgClosed` `IsAlgClosure.isAlgebraic`

---

← Back to Index