Algebra

📁 Source: Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

Statistics

Metric	Count
Definitions adjoinAlgebraMapOfAlgebra, instAlgebraSubtypeMemSubalgebraAdjoinAdjoin, instAlgebraSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap	3
Theorems adjoin_eq_top_of_intermediateField, adjoin_eq_top_of_primitive_element, finite_of_essFiniteType_of_isAlgebraic, isIntegral_gen, adjoin_algebraic_toSubalgebra, adjoin_eq_algebra_adjoin, adjoin_eq_top_iff, adjoin_eq_top_iff_of_isAlgebraic, adjoin_eq_top_of_algebra, adjoin_intermediateField_toSubalgebra_of_isAlgebraic, adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left, adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right, adjoin_simple_eq_top_iff_of_isAlgebraic, adjoin_simple_toSubalgebra_of_integral, adjoin_simple_toSubalgebra_of_isAlgebraic, adjoin_toSubalgebra, adjoin_toSubalgebra_of_isAlgebraic, adjoin_toSubalgebra_of_isAlgebraic_left, adjoin_toSubalgebra_of_isAlgebraic_right, instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, algebra_adjoin_le_adjoin, eq_adjoin_of_eq_algebra_adjoin, essFiniteType_iff, fg_of_fg_toSubalgebra, fg_of_noetherian, fg_top, fg_top_iff, finite_of_fg_of_isAlgebraic, induction_on_adjoin, instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap, le_sup_toSubalgebra, sup_toSubalgebra_of_isAlgebraic, sup_toSubalgebra_of_isAlgebraic_left, sup_toSubalgebra_of_isAlgebraic_right, sup_toSubalgebra_of_left, sup_toSubalgebra_of_right, algHom_fieldRange_eq_of_comp_eq, algHom_fieldRange_eq_of_comp_eq_of_range_eq, liftAlgHom_fieldRange, liftAlgHom_fieldRange_eq_of_range_eq	44
Total	47

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_top_of_intermediateField 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing IntermediateField.adjoin Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subalgebra instCompleteLatticeSubalgebra	—	IntermediateField.adjoin_eq_top_iff_of_isAlgebraic
adjoin_eq_top_of_primitive_element 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing IntermediateField.adjoin Set Set.instSingletonSet Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subalgebra instCompleteLatticeSubalgebra	—	IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic
finite_of_essFiniteType_of_isAlgebraic 📖	mathematical	—	Module.Finite DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toModule Semifield.toCommSemiring	—	IntermediateField.fg_top IntermediateField.adjoin_toSubalgebra_of_isAlgebraic IsAlgebraic.isAlgebraic IntermediateField.adjoin_toSubalgebra IsIntegral.finite IsAlgebraic.isIntegral

IntermediateField

Definitions

Name	Category	Theorems
instAlgebraSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap 📖	CompOp	1 math math: instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_algebraic_toSubalgebra 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	toSubalgebra adjoin Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	adjoin_toSubalgebra_of_isAlgebraic
adjoin_eq_algebra_adjoin 📖	mathematical	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	toSubalgebra adjoin	—	le_antisymm adjoin_le_iff Algebra.subset_adjoin algebra_adjoin_le_adjoin
adjoin_eq_top_iff 📖	mathematical	—	adjoin Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subalgebra Algebra.instCompleteLatticeSubalgebra	—	adjoin_eq_top_iff_of_isAlgebraic Algebra.IsAlgebraic.isAlgebraic
adjoin_eq_top_iff_of_isAlgebraic 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	adjoin Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subalgebra Algebra.instCompleteLatticeSubalgebra	—	adjoin_toSubalgebra_of_isAlgebraic top_toSubalgebra
adjoin_eq_top_of_algebra 📖	mathematical	Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	adjoin IntermediateField instCompleteLattice	—	top_le_iff Eq.trans_le algebra_adjoin_le_adjoin
adjoin_intermediateField_toSubalgebra_of_isAlgebraic 📖	mathematical	Algebra.IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing IntermediateField SetLike.instMembership instSetLike toField algebra' CommRing.toCommSemiring Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule	toSubalgebra adjoin SetLike.coe Algebra.adjoin	—	IsScalarTower.left IsLocalRing.toNontrivial Field.instIsLocalRing SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass Subalgebra.restrictScalars_injective restrictScalars_toSubalgebra isScalarTower_mid' restrictScalars_adjoin_of_algEquiv Algebra.restrictScalars_adjoin_of_algEquiv restrictScalars_adjoin IsScalarTower.subalgebra' IsScalarTower.right Algebra.restrictScalars_adjoin sup_toSubalgebra_of_isAlgebraic AlgEquiv.isAlgebraic
adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left 📖	mathematical	—	toSubalgebra adjoin SetLike.coe IntermediateField instSetLike Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	adjoin_intermediateField_toSubalgebra_of_isAlgebraic IsScalarTower.left
adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right 📖	mathematical	—	toSubalgebra adjoin SetLike.coe IntermediateField instSetLike Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	IsScalarTower.left adjoin_intermediateField_toSubalgebra_of_isAlgebraic
adjoin_simple_eq_top_iff_of_isAlgebraic 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	adjoin Set Set.instSingletonSet Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subalgebra Algebra.instCompleteLatticeSubalgebra	—	adjoin_eq_top_iff_of_isAlgebraic
adjoin_simple_toSubalgebra_of_integral 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	toSubalgebra adjoin Set Set.instSingletonSet Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	adjoin_toSubalgebra_of_isAlgebraic
adjoin_simple_toSubalgebra_of_isAlgebraic 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	toSubalgebra adjoin Set Set.instSingletonSet Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	adjoin_toSubalgebra_of_isAlgebraic
adjoin_toSubalgebra 📖	mathematical	—	toSubalgebra adjoin Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	adjoin_toSubalgebra_of_isAlgebraic Algebra.IsAlgebraic.isAlgebraic
adjoin_toSubalgebra_of_isAlgebraic 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	toSubalgebra adjoin Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	adjoin_eq_algebra_adjoin Algebra.IsIntegral.inv_mem Algebra.IsIntegral.adjoin IsAlgebraic.isIntegral
adjoin_toSubalgebra_of_isAlgebraic_left 📖	mathematical	—	toSubalgebra adjoin SetLike.coe IntermediateField instSetLike Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left
adjoin_toSubalgebra_of_isAlgebraic_right 📖	mathematical	—	toSubalgebra adjoin SetLike.coe IntermediateField instSetLike Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right
algebra_adjoin_le_adjoin 📖	mathematical	—	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Algebra.adjoin toSubalgebra adjoin	—	Algebra.adjoin_le subset_adjoin
eq_adjoin_of_eq_algebra_adjoin 📖	mathematical	toSubalgebra Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	adjoin	—	toSubalgebra_injective adjoin_eq_algebra_adjoin inv_mem
essFiniteType_iff 📖	mathematical	—	Algebra.EssFiniteType IntermediateField SetLike.instMembership instSetLike EuclideanDomain.toCommRing Field.toEuclideanDomain toField algebra' CommRing.toCommSemiring Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule FG	—	subset_adjoin IsScalarTower.left map_injective adjoin_map Set.image_congr fieldRange_val Equiv.exists_congr_left Finset.coe_map Finset.coe_attach Set.image_univ Subtype.range_coe_subtype
fg_of_fg_toSubalgebra 📖	mathematical	Subalgebra.FG Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toSubalgebra	FG	—	eq_adjoin_of_eq_algebra_adjoin
fg_of_noetherian 📖	mathematical	—	FG	—	fg_of_fg_toSubalgebra Subalgebra.fg_of_noetherian
fg_top 📖	mathematical	—	FG Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	fg_top_iff
fg_top_iff 📖	mathematical	—	FG Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Algebra.EssFiniteType EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Algebra.FiniteType.adjoin_of_finite Finset.finite_toSet Algebra.EssFiniteType.of_isLocalization algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin IsScalarTower.left Algebra.EssFiniteType.comp algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin Algebra.EssFiniteType.of_finiteType Algebra.EssFiniteType.of_surjective AlgEquiv.surjective top_le_iff Algebra.EssFiniteType.isLocalization IsLocalization.exists_mk'_eq IsUnit.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing IsLocalization.map_units IsUnit.div_mul_cancel div_mem SubfieldClass.toSubgroupClass instSubfieldClass algebra_adjoin_le_adjoin
finite_of_fg_of_isAlgebraic 📖	mathematical	—	Module.Finite DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	—	Algebra.finite_of_essFiniteType_of_isAlgebraic
induction_on_adjoin 📖	—	Bot.bot IntermediateField OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder restrictScalars SetLike.instMembership instSetLike toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule instAlgebraSubtypeMem isScalarTower_mid' adjoin Set Set.instSingletonSet	—	—	IsScalarTower.left isScalarTower_mid' induction_on_adjoin_fg fg_of_noetherian IsNoetherian.iff_fg
instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap 📖	mathematical	—	IsScalarTower Subalgebra Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet IntermediateField instSetLike adjoin DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Algebra.toSMul Polynomial.instCommSemiringAdjoinSingleton toField instAlgebraSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap instSMulSubtypeMem Algebra.id Subalgebra.instSMulSubtypeMem	—	IsScalarTower.of_algebraMap_eq' SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
le_sup_toSubalgebra 📖	mathematical	—	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra toSubalgebra IntermediateField instCompleteLattice	—	sup_le le_sup_left le_sup_right
sup_toSubalgebra_of_isAlgebraic 📖	mathematical	Algebra.IsAlgebraic IntermediateField SetLike.instMembership instSetLike EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing toField algebra' CommRing.toCommSemiring Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule	toSubalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Subalgebra Algebra.instCompleteLatticeSubalgebra	—	IsScalarTower.left sup_toSubalgebra_of_isAlgebraic_left sup_toSubalgebra_of_isAlgebraic_right
sup_toSubalgebra_of_isAlgebraic_left 📖	mathematical	—	toSubalgebra IntermediateField SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.instCompleteLatticeSubalgebra	—	IsScalarTower.left sup_toSubalgebra_of_isAlgebraic_right sup_comm
sup_toSubalgebra_of_isAlgebraic_right 📖	mathematical	—	toSubalgebra IntermediateField SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.instCompleteLatticeSubalgebra	—	IsScalarTower.left adjoin_toSubalgebra_of_isAlgebraic IsAlgebraic.tower_top isScalarTower_mid' isAlgebraic_iff Algebra.IsAlgebraic.isAlgebraic IsScalarTower.subalgebra' IsScalarTower.right Algebra.restrictScalars_adjoin restrictScalars_adjoin restrictScalars_toSubalgebra
sup_toSubalgebra_of_left 📖	mathematical	—	toSubalgebra IntermediateField SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.instCompleteLatticeSubalgebra	—	IsScalarTower.left sup_toSubalgebra_of_isAlgebraic_left Algebra.IsAlgebraic.of_finite IsLocalRing.toNontrivial Field.instIsLocalRing
sup_toSubalgebra_of_right 📖	mathematical	—	toSubalgebra IntermediateField SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.instCompleteLatticeSubalgebra	—	IsScalarTower.left sup_toSubalgebra_of_isAlgebraic_right Algebra.IsAlgebraic.of_finite IsLocalRing.toNontrivial Field.instIsLocalRing

IntermediateField.AdjoinSimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral_gen 📖	mathematical	—	IsIntegral IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing IntermediateField.toField IntermediateField.algebra' CommRing.toCommSemiring Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule gen	—	IsScalarTower.left SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass algebraMap_gen isIntegral_algebraMap_iff IntermediateField.isScalarTower_mid' RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing

IntermediateField.RingHom

Definitions

Name	Category	Theorems
adjoinAlgebraMapOfAlgebra 📖	CompOp	—

IntermediateField.algebraAdjoinAdjoin

Definitions

Name	Category	Theorems
instAlgebraSubtypeMemSubalgebraAdjoinAdjoin 📖	CompOp	5 math math: instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin 📖	mathematical	—	FaithfulSMul Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin IntermediateField IntermediateField.instSetLike IntermediateField.adjoin Algebra.toSMul Subalgebra.toCommSemiring IntermediateField.toField instAlgebraSubtypeMemSubalgebraAdjoinAdjoin	—	Subalgebra.inclusion.faithfulSMul IntermediateField.algebra_adjoin_le_adjoin
instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin 📖	mathematical	—	Algebra.IsAlgebraic Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin IntermediateField IntermediateField.instSetLike IntermediateField.adjoin Subalgebra.toCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing IntermediateField.toField instAlgebraSubtypeMemSubalgebraAdjoinAdjoin	—	IsLocalization.isAlgebraic SubsemiringClass.nontrivial Subalgebra.instSubsemiringClass IsLocalRing.toNontrivial Field.instIsLocalRing instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin
instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin 📖	mathematical	—	IsFractionRing Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Subalgebra.toCommSemiring IntermediateField IntermediateField.instSetLike IntermediateField.adjoin SubsemiringClass.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing SubfieldClass.toSubringClass IntermediateField.instSubfieldClass instAlgebraSubtypeMemSubalgebraAdjoinAdjoin	—	IsFractionRing.of_field instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin IntermediateField.mem_adjoin_iff_div
instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin 📖	mathematical	—	IsScalarTower Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin IntermediateField IntermediateField.instSetLike IntermediateField.adjoin SetLike.smul' 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 Subalgebra.instSMulMemClass Algebra.toSMul Subalgebra.toCommSemiring IntermediateField.toField instAlgebraSubtypeMemSubalgebraAdjoinAdjoin IntermediateField.instSMulMemClass	—	Subalgebra.inclusion.isScalarTower_left IntermediateField.algebra_adjoin_le_adjoin
instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1 📖	mathematical	—	IsScalarTower Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin IntermediateField IntermediateField.instSetLike IntermediateField.adjoin Algebra.toSMul Subalgebra.toCommSemiring IntermediateField.toField instAlgebraSubtypeMemSubalgebraAdjoinAdjoin IntermediateField.instSMulSubtypeMem SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction Subalgebra.instSMulSubtypeMem	—	Subalgebra.inclusion.isScalarTower_right IntermediateField.algebra_adjoin_le_adjoin

IsFractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom_fieldRange_eq_of_comp_eq 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHomClass.toRingHom AlgHom Semifield.toCommSemiring AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass algebraMap	AlgHom.fieldRange IntermediateField.adjoin SetLike.coe Subalgebra Subalgebra.instSetLike AlgHom.range	—	AlgHomClass.toRingHomClass AlgHom.algHomClass IntermediateField.toSubfield_injective Set.union_eq_self_of_subset_left AlgHom.commutes ringHom_fieldRange_eq_of_comp_eq
algHom_fieldRange_eq_of_comp_eq_of_range_eq 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHomClass.toRingHom AlgHom Semifield.toCommSemiring AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass algebraMap AlgHom.range Algebra.adjoin	AlgHom.fieldRange IntermediateField.adjoin	—	AlgHomClass.toRingHomClass AlgHom.algHomClass IntermediateField.toSubfield_injective ringHom_fieldRange_eq_of_comp_eq_of_range_eq Algebra.adjoin_eq_ring_closure
liftAlgHom_fieldRange 📖	mathematical	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike	AlgHom.fieldRange liftAlgHom EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.adjoin SetLike.coe Subalgebra Subalgebra.instSetLike AlgHom.range	—	algHom_fieldRange_eq_of_comp_eq RingHom.ext AlgHomClass.toRingHomClass AlgHom.algHomClass lift_algebraMap
liftAlgHom_fieldRange_eq_of_range_eq 📖	mathematical	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike AlgHom.range Algebra.adjoin	AlgHom.fieldRange liftAlgHom EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.adjoin	—	algHom_fieldRange_eq_of_comp_eq_of_range_eq RingHom.ext AlgHomClass.toRingHomClass AlgHom.algHomClass lift_algebraMap

---

← Back to Index