Isaacs

📁 Source: Mathlib/FieldTheory/Isaacs.lean

Statistics

Metric	Count
Definitions	0
Theorems nonempty_algEquiv_of_aeval_eq_zero_eq, nonempty_algEquiv_of_range_minpoly_eq, nonempty_algHom_of_aeval_eq_zero_subset, nonempty_algHom_of_exist_roots, nonempty_algHom_of_exists_root, nonempty_algHom_of_minpoly_eq, nonempty_algHom_of_range_minpoly_subset, of_exist_roots, of_exists_root	9
Total	9

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_algEquiv_of_aeval_eq_zero_eq 📖	mathematical	setOf Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring toSemifield DFunLike.coe AlgHom CommSemiring.toSemiring Semifield.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing toEuclideanDomain	AlgEquiv	—	nonempty_algHom_of_aeval_eq_zero_subset Eq.le Eq.ge Algebra.IsAlgebraic.algHom_bijective₂ instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
nonempty_algEquiv_of_range_minpoly_eq 📖	mathematical	Set.range Polynomial CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing toEuclideanDomain minpoly DivisionRing.toRing toDivisionRing	AlgEquiv Semifield.toCommSemiring toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	nonempty_algHom_of_range_minpoly_subset Eq.le IsIntegral.isAlgebraic IsLocalRing.toNontrivial instIsLocalRing Eq.ge minpoly.ne_zero Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral minpoly.eq_zero Algebra.IsAlgebraic.algHom_bijective₂ instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
nonempty_algHom_of_aeval_eq_zero_subset 📖	—	Set Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring toSemifield Set.instHasSubset setOf DFunLike.coe AlgHom CommSemiring.toSemiring Semifield.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing toEuclideanDomain	—	—	nonempty_algHom_of_minpoly_eq minpoly.aeval minpoly.eq_iff_aeval_minpoly_eq_zero instIsDomain IsLocalRing.toNontrivial instIsLocalRing Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral
nonempty_algHom_of_exist_roots 📖	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring toSemifield Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly EuclideanDomain.toCommRing toEuclideanDomain DivisionRing.toRing toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	nonempty_algHom_of_exists_root
nonempty_algHom_of_exists_root 📖	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring toSemifield Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly EuclideanDomain.toCommRing toEuclideanDomain DivisionRing.toRing toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	IntermediateField.Lifts.nonempty_algHom_of_exist_lifts_finset Polynomial.Splits.of_dvd instIsDomain Polynomial.SplittingField.splits Polynomial.map_ne_zero DivisionRing.isSimpleRing IsLocalRing.toNontrivial instIsLocalRing Finset.prod_ne_zero_iff Polynomial.nontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors minpoly.ne_zero Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral IsScalarTower.algebraMap_eq Polynomial.map_map Polynomial.map_dvd_map' Finset.dvd_prod_of_mem IsScalarTower.left IntermediateField.finiteDimensional_adjoin Finite.of_fintype Set.eq_univ_of_forall Set.mem_iUnion IntermediateField.adjoin_simple_le_iff IntermediateField.exists_algHom_adjoin_of_splits DFunLike.congr_fun AlgHom.comp_apply AlgEquiv.coe_algHom IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen AdjoinRoot.liftAlgHom_root finite_or_infinite exists_primitive_element_of_finite_bot Set.mem_univ Subspace.exists_eq_top_of_iUnion_eq_univ Finite.algHom Module.Free.of_divisionRing IntermediateField.isScalarTower IsScalarTower.right IntermediateField.subset_adjoin
nonempty_algHom_of_minpoly_eq 📖	mathematical	minpoly EuclideanDomain.toCommRing toEuclideanDomain DivisionRing.toRing toDivisionRing	AlgHom Semifield.toCommSemiring toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	nonempty_algHom_of_exists_root minpoly.aeval
nonempty_algHom_of_range_minpoly_subset 📖	mathematical	Set Polynomial CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing toEuclideanDomain Set.instHasSubset Set.range minpoly DivisionRing.toRing toDivisionRing	AlgHom Semifield.toCommSemiring toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	nonempty_algHom_of_minpoly_eq

IsAlgClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_exist_roots 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	IsAlgClosure instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommRing.toCommSemiring instIsDomain Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Algebra.toModule GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	of_exists_root
of_exists_root 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	IsAlgClosure instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommRing.toCommSemiring instIsDomain Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Algebra.toModule GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	of_splits instIsDomain Algebra.IsAlgebraic.isIntegral instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Field.nonempty_algHom_of_exists_root Normal.toIsAlgebraic Polynomial.SplittingField.instNormal Algebra.IsIntegral.isIntegral minpoly.monic minpoly.irreducible Polynomial.Splits.of_algHom Polynomial.SplittingField.splits

---

← Back to Index