Luroth

📁 Source: Mathlib/FieldTheory/RatFunc/Luroth.lean

Statistics

Metric	Count
Definitions adjoinXEquiv, algEquiv, generator, minpolyX	4
Theorems C_minpolyX, adjoin_X, isAlgebraic_X, adjoin_generator_le, algEquiv_X, algEquiv_algebraMap, algEquiv_apply, eq_adjoin_generator, generator_eq_zero, generator_mem, generator_ne_C, generator_ne_zero, generator_spec, transcendental_generator, adjoin_X, eq_C_of_minpolyX_coeff_eq_zero, finrank_eq_max_natDegree, irreducible_minpolyX, irreducible_minpolyX', isAlgebraic_adjoin_simple_X, isAlgebraic_adjoin_simple_X', minpolyX_aeval_X, minpolyX_eq_zero_iff, minpolyX_map, natDegree_denom_le_natDegree_minpolyX, natDegree_minpolyX, natDegree_num_le_natDegree_minpolyX, transcendental_of_ne_C	28
Total	32

RatFunc

Definitions

Name	Category	Theorems
minpolyX 📖	CompOp	9 math math: minpolyX_map, minpolyX_aeval_X, irreducible_minpolyX, natDegree_minpolyX, irreducible_minpolyX', minpolyX_eq_zero_iff, natDegree_num_le_natDegree_minpolyX, C_minpolyX, natDegree_denom_le_natDegree_minpolyX

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_minpolyX 📖	mathematical	—	minpolyX DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C IntermediateField instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField IntermediateField.algebra' Algebra.toSMul instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin Polynomial Polynomial.instZero	—	instIsDomain instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right num_C Polynomial.map_C denom_C Polynomial.map_one mul_one
adjoin_X 📖	mathematical	—	IntermediateField.adjoin RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id Set Set.instSingletonSet X Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instIsDomain eq_top_iff IntermediateField.mem_adjoin_simple_iff aeval_X_left_eq_algebraMap num_div_denom
eq_C_of_minpolyX_coeff_eq_zero 📖	mathematical	RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet Polynomial.coeff IntermediateField.toField minpolyX IntermediateField.algebra' Algebra.toSMul instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring denom instZero	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	—	instIsDomain instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eq_div_iff map_ne_zero instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.leadingCoeff_ne_zero denom_ne_zero Polynomial.coeff_sub Polynomial.coeff_map Polynomial.coeff_C_mul
finrank_eq_max_natDegree 📖	mathematical	—	Module.finrank RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing IntermediateField.instModuleSubtypeMem Semiring.toModule Polynomial.natDegree num denom	—	instIsDomain IntermediateField.adjoin_simple_eq_bot_iff IntermediateField.finrank_bot' Module.finrank_of_not_finite commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing Algebra.transcendental_iff_not_isAlgebraic transcendental Algebra.IsAlgebraic.of_finite num_C Polynomial.natDegree_C denom_C Polynomial.natDegree_one max_self SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass LinearEquiv.finrank_eq IsScalarTower.left IntermediateField.adjoin.finrank IsAlgebraic.isIntegral isAlgebraic_adjoin_simple_X instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right minpoly.eq_of_irreducible instNontrivial irreducible_minpolyX minpolyX_aeval_X mul_comm Polynomial.natDegree_C_mul SubsemiringClass.noZeroDivisors IsDomain.to_noZeroDivisors inv_ne_zero Polynomial.leadingCoeff_ne_zero minpolyX_eq_zero_iff natDegree_minpolyX
irreducible_minpolyX 📖	mathematical	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	Irreducible Polynomial RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring minpolyX IntermediateField.algebra' Algebra.toSMul instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin	—	instIsDomain instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right minpolyX_map IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin IsScalarTower.left Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin Subalgebra.isDomain instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid Transcendental.uniqueFactorizationMonoid_adjoin PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain transcendental_of_ne_C Irreducible.isPrimitive Subalgebra.noZeroDivisors IsDomain.to_noZeroDivisors irreducible_minpolyX' Polynomial.natDegree_map_le eq_C_iff natDegree_minpolyX nonpos_iff_eq_zero Nat.instCanonicallyOrderedAdd
irreducible_minpolyX' 📖	mathematical	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	Irreducible Polynomial RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring instField instIsDomain instAlgebraOfPolynomial Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet Algebra.instCommRingAdjoinSingleton DivisionRing.toRing Field.toDivisionRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring minpolyX Subalgebra.algebra Algebra.instCommSemiringAdjoinSingleton	—	instIsDomain transcendental_of_ne_C AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.self_mem_adjoin_singleton AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass map_sub RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Polynomial.map_map map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass Polynomial.map_C Polynomial.aeval_X RingHom.ext Polynomial.aeval_C Polynomial.ext Polynomial.coeff_map MulEquiv.irreducible_iff RingEquivClass.toMulEquivClass Polynomial.X_mul_C Polynomial.aeval_sub NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass Polynomial.eval_sub Polynomial.eval_map_algebraMap Polynomial.eval_mul Polynomial.eval_C mul_comm add_comm map_neg RingHom.instRingHomClass neg_mul sub_eq_add_neg Polynomial.irreducible_C_mul_X_add_C Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd neg_ne_zero denom_ne_zero IsCoprime.isRelPrime IsCoprime.symm IsCoprime.neg_right_iff isCoprime_num_denom
isAlgebraic_adjoin_simple_X 📖	mathematical	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	IsAlgebraic RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField DivisionRing.toRing Field.toDivisionRing IntermediateField.instAlgebraSubtypeMem Ring.toSemiring X	—	instIsDomain instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right minpolyX_eq_zero_iff minpolyX_aeval_X
isAlgebraic_adjoin_simple_X' 📖	mathematical	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	Algebra.IsAlgebraic RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField DivisionRing.toRing Field.toDivisionRing IntermediateField.instAlgebraSubtypeMem Ring.toSemiring	—	instIsDomain IntermediateField.isAlgebraic_adjoin_simple isAlgebraic_iff_isIntegral isAlgebraic_adjoin_simple_X AlgEquiv.isAlgebraic
minpolyX_aeval_X 📖	mathematical	—	DFunLike.coe AlgHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet Polynomial SubsemiringClass.toCommSemiring SubringClass.toSubsemiringClass NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing instCommRing SubfieldClass.toSubringClass Field.toDivisionRing IntermediateField.instSubfieldClass Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.instAlgebraSubtypeMem AlgHom.funLike Polynomial.aeval X minpolyX IntermediateField.toField IntermediateField.algebra' Algebra.toSMul instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin instZero	—	instIsDomain SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right Polynomial.aeval_sub Polynomial.aeval_map_algebraMap IntermediateField.isScalarTower_mid' aeval_X_left_eq_algebraMap map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.aeval_C num_div_denom div_mul_cancel₀ algebraMap_ne_zero denom_ne_zero sub_self
minpolyX_eq_zero_iff 📖	mathematical	—	minpolyX RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField IntermediateField.algebra' Algebra.toSMul instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin Polynomial Polynomial.instZero DFunLike.coe RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike C	—	instIsDomain instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right eq_C_of_minpolyX_coeff_eq_zero C_minpolyX
minpolyX_map 📖	mathematical	—	Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring algebraMap minpolyX	—	instIsDomain Polynomial.map_sub Polynomial.map_map Polynomial.map_mul Polynomial.map_C
natDegree_denom_le_natDegree_minpolyX 📖	mathematical	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield denom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField minpolyX IntermediateField.algebra' Algebra.toSMul instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin	—	instIsDomain Polynomial.le_natDegree_of_ne_zero instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right eq_C_of_minpolyX_coeff_eq_zero
natDegree_minpolyX 📖	mathematical	—	Polynomial.natDegree RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain Field.toSemifield instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField minpolyX IntermediateField.algebra' Algebra.toSMul instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin DivisionSemiring.toSemiring Semifield.toDivisionSemiring num denom	—	instIsDomain instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right C_minpolyX num_C Polynomial.natDegree_C denom_C Polynomial.natDegree_one max_self le_antisymm Polynomial.natDegree_sub_le Polynomial.natDegree_map DivisionRing.isSimpleRing SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.natDegree_C_mul SubsemiringClass.noZeroDivisors IsDomain.to_noZeroDivisors map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass max_le natDegree_num_le_natDegree_minpolyX Polynomial.le_natDegree_of_ne_zero eq_C_of_minpolyX_coeff_eq_zero
natDegree_num_le_natDegree_minpolyX 📖	mathematical	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield num RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField instField instIsDomain instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet IntermediateField.toField minpolyX IntermediateField.algebra' Algebra.toSMul instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin	—	instIsDomain RingHom.map_zero Polynomial.le_natDegree_of_ne_zero instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_div₀ inv_inv eq_div_iff map_ne_zero instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.leadingCoeff_ne_zero num_ne_zero one_mul inv_mul_cancel₀ mul_assoc mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero inv_ne_zero sub_eq_zero Polynomial.coeff_sub Polynomial.coeff_map Polynomial.coeff_C_mul
transcendental_of_ne_C 📖	mathematical	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	Transcendental RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing instField instIsDomain Field.toSemifield instAlgebraOfPolynomial CommRing.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring Algebra.id	—	instIsDomain IsScalarTower.left IntermediateField.isAlgebraic_adjoin_simple IsAlgebraic.isIntegral transcendental Algebra.transcendental_iff_not_isAlgebraic Algebra.IsAlgebraic.trans instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right IntermediateField.isScalarTower_mid' SubsemiringClass.noZeroDivisors SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsDomain.to_noZeroDivisors isAlgebraic_adjoin_simple_X'

RatFunc.IntermediateField

Definitions

Name	Category	Theorems
adjoinXEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_X 📖	mathematical	—	IntermediateField.adjoin RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField IntermediateField.instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set Set.instSingletonSet RatFunc.X Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instIsDomain RatFunc.instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right IntermediateField.isScalarTower_mid' IntermediateField.restrictScalars_eq_top_iff IsScalarTower.left IntermediateField.restrictScalars_adjoin eq_top_iff le_trans le_of_eq RatFunc.adjoin_X IntermediateField.adjoin.mono Set.union_singleton
isAlgebraic_X 📖	mathematical	—	IsAlgebraic RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField DivisionRing.toRing Field.toDivisionRing IntermediateField.instAlgebraSubtypeMem Ring.toSemiring RatFunc.X	—	instIsDomain SetLike.not_le_iff_exists instIsConcreteLE le_bot_iff IsAlgebraic.tower_top_of_subalgebra_le IntermediateField.adjoin_simple_le_iff RatFunc.isAlgebraic_adjoin_simple_X

RatFunc.Luroth

Definitions

Name	Category	Theorems
algEquiv 📖	CompOp	3 math math: algEquiv_apply, algEquiv_algebraMap, algEquiv_X
generator 📖	CompOp	10 math math: algEquiv_apply, algEquiv_algebraMap, generator_mem, generator_ne_C, eq_adjoin_generator, algEquiv_X, generator_eq_zero, adjoin_generator_le, transcendental_generator, generator_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_generator_le 📖	mathematical	—	IntermediateField RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder IntermediateField.adjoin Set Set.instSingletonSet generator	—	instIsDomain IntermediateField.adjoin_simple_le_iff generator_mem
algEquiv_X 📖	mathematical	—	RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike DFunLike.coe AlgEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul RatFunc.instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right AlgEquiv.instFunLike algEquiv RatFunc.X generator	—	instIsDomain RatFunc.instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right RatFunc.algEquivOfTranscendental_X
algEquiv_algebraMap 📖	mathematical	—	RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike DFunLike.coe AlgEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul RatFunc.instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right AlgEquiv.instFunLike algEquiv RingHom Polynomial Polynomial.commSemiring RingHom.instFunLike algebraMap AlgHom Polynomial.semiring AlgHom.funLike Polynomial.aeval generator	—	instIsDomain RatFunc.instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right IsScalarTower.left IntermediateField.AdjoinSimple.coe_aeval_gen_apply RatFunc.algEquivOfTranscendental_algebraMap
algEquiv_apply 📖	mathematical	—	RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike DFunLike.coe AlgEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul RatFunc.instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right AlgEquiv.instFunLike algEquiv RatFunc.instDiv AlgHom Polynomial Polynomial.semiring AlgHom.funLike Polynomial.aeval generator RatFunc.num RatFunc.denom	—	instIsDomain RatFunc.instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right RatFunc.algEquivOfTranscendental_apply
eq_adjoin_generator 📖	mathematical	—	IntermediateField.adjoin RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id Set Set.instSingletonSet generator	—	instIsDomain generator_eq_zero IntermediateField.adjoin_zero le_antisymm IntermediateField.relfinrank_eq_one_iff mul_eq_right₀ IsCancelMulZero.toIsRightCancelMulZero Nat.instIsCancelMulZero generator_ne_C RatFunc.eq_C_iff IntermediateField.relfinrank_mul_finrank_top adjoin_generator_le RatFunc.finrank_eq_max_natDegree
generator_eq_zero 📖	mathematical	Bot.bot IntermediateField RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	generator RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instZero	—	instIsDomain
generator_mem 📖	mathematical	—	RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial Semifield.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id SetLike.instMembership IntermediateField.instSetLike generator	—	instIsDomain generator_eq_zero IntermediateField.zero_mem SetLike.coe_mem
generator_ne_C 📖	mathematical	—	generator DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RatFunc.instField instIsDomain RingHom.instFunLike RatFunc.C	—	instIsDomain generator_spec
generator_ne_zero 📖	—	—	—	—	instIsDomain generator_ne_C map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
generator_spec 📖	mathematical	—	RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing RatFunc.instCommRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RatFunc.instField instIsDomain RatFunc.instAlgebraOfPolynomial Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id generator	—	instIsDomain RatFunc.instIsScalarTowerOfIsDomainOfPolynomial Polynomial.isScalarTower IsScalarTower.right
transcendental_generator 📖	mathematical	—	Transcendental RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring Algebra.id generator	—	instIsDomain RatFunc.transcendental_of_ne_C generator_ne_C

---

← Back to Index