Algebraic

📁 Source: Mathlib/FieldTheory/IntermediateField/Algebraic.lean

Statistics

Metric	Count
Definitions toIntermediateField, toIntermediateField, subalgebraEquivIntermediateField	3
Theorems coe_isIntegral_iff, eq_of_le_of_finrank_eq, eq_of_le_of_finrank_eq', eq_of_le_of_finrank_le, eq_of_le_of_finrank_le', finiteDimensional_left, finiteDimensional_map, finiteDimensional_right, finrank_dvd_of_le_left, finrank_dvd_of_le_right, finrank_eq_finrank_subalgebra, finrank_le_of_le_left, finrank_le_of_le_right, finrank_lt_of_gt, isAlgebraic_iff, isAlgebraic_tower_bot, isAlgebraic_tower_top, isIntegral_iff, minpoly_eq, rank_eq_rank_subalgebra, mem_subalgebraEquivIntermediateField, mem_subalgebraEquivIntermediateField_symm	22
Total	25

Algebra.IsAlgebraic

Definitions

Name	Category	Theorems
toIntermediateField 📖	CompOp	—

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_isIntegral_iff 📖	mathematical	—	IsIntegral DivisionRing.toRing Field.toDivisionRing IntermediateField SetLike.instMembership instSetLike toField algebra' CommRing.toCommSemiring Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	isIntegral_algHom_iff IsScalarTower.left isScalarTower Subtype.val_injective
eq_of_le_of_finrank_eq 📖	—	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toField module' Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—	IsScalarTower.left eq_of_le_of_finrank_le Eq.ge
eq_of_le_of_finrank_eq' 📖	—	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	—	eq_of_le_of_finrank_le' Eq.le
eq_of_le_of_finrank_le 📖	—	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toField module' Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—	IsScalarTower.left toSubalgebra_injective Subalgebra.eq_of_le_of_finrank_le
eq_of_le_of_finrank_le' 📖	—	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	—	le_antisymm le_refl mem_extendScalars extendScalars_le_extendScalars_iff
finiteDimensional_left 📖	mathematical	—	FiniteDimensional IntermediateField SetLike.instMembership instSetLike Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing toField module' DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id Algebra.toModule Semifield.toDivisionSemiring 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	—	FiniteDimensional.left IsScalarTower.left instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isScalarTower_mid' EuclideanDomain.toNontrivial
finiteDimensional_map 📖	mathematical	—	FiniteDimensional IntermediateField SetLike.instMembership instSetLike map Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing toField module' DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id Algebra.toModule Semifield.toDivisionSemiring 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	—	IsScalarTower.left LinearEquiv.finiteDimensional
finiteDimensional_right 📖	mathematical	—	FiniteDimensional IntermediateField SetLike.instMembership instSetLike Field.toDivisionRing toField Ring.toAddCommGroup DivisionRing.toRing instModuleSubtypeMem AddCommGroup.toAddCommMonoid Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	FiniteDimensional.right IsScalarTower.left isScalarTower_mid'
finrank_dvd_of_le_left 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left IsScalarTower.of_algebraMap_eq Dvd.intro_left Module.finrank_mul_finrank commRing_strongRankCondition SubsemiringClass.nontrivial EuclideanDomain.toNontrivial Module.Free.of_divisionRing
finrank_dvd_of_le_right 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toField module' Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left Dvd.intro Module.finrank_mul_finrank IsScalarTower.of_algHom commRing_strongRankCondition EuclideanDomain.toNontrivial SubsemiringClass.nontrivial Module.Free.of_divisionRing
finrank_eq_finrank_subalgebra 📖	mathematical	—	Module.finrank Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike toSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subalgebra.instModuleSubtypeMem IntermediateField instSetLike toField module' Algebra.toSMul CommSemiring.toSemiring Algebra.id Algebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—
finrank_le_of_le_left 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	Module.finrank_pos commRing_strongRankCondition SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass EuclideanDomain.toNontrivial instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors finrank_dvd_of_le_left
finrank_le_of_le_right 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toField module' Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left Module.finrank_pos commRing_strongRankCondition EuclideanDomain.toNontrivial instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass finrank_dvd_of_le_right
finrank_lt_of_gt 📖	mathematical	IntermediateField Preorder.toLT PartialOrder.toPreorder instPartialOrder	Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left LT.lt.le IsScalarTower.of_algebraMap_eq' lt_of_le_of_ne Module.finrank_top_le_finrank_of_isScalarTower commRing_strongRankCondition SubsemiringClass.nontrivial EuclideanDomain.toNontrivial IsScalarTower.right Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing eq_of_le_of_finrank_eq' LT.lt.ne
isAlgebraic_iff 📖	mathematical	—	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	—	IsScalarTower.left isAlgebraic_algebraMap_iff isScalarTower_mid' RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
isAlgebraic_tower_bot 📖	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	—	Algebra.IsAlgebraic.of_injective IsScalarTower.left RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial
isAlgebraic_tower_top 📖	mathematical	—	Algebra.IsAlgebraic IntermediateField SetLike.instMembership instSetLike EuclideanDomain.toCommRing Field.toEuclideanDomain toField DivisionRing.toRing Field.toDivisionRing instAlgebraSubtypeMem Ring.toSemiring Algebra.id Semifield.toCommSemiring Field.toSemifield	—	Algebra.IsAlgebraic.tower_top IsScalarTower.left isScalarTower_mid'
isIntegral_iff 📖	mathematical	—	IsIntegral 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	—	IsScalarTower.left isIntegral_algHom_iff RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial
minpoly_eq 📖	mathematical	—	minpoly 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	—	IsScalarTower.left minpoly.algebraMap_eq isScalarTower_mid' RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
rank_eq_rank_subalgebra 📖	mathematical	—	Module.rank Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike toSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subalgebra.instModuleSubtypeMem IntermediateField instSetLike toField module' Algebra.toSMul CommSemiring.toSemiring Algebra.id Algebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—

Subalgebra.IsAlgebraic

Definitions

Name	Category	Theorems
toIntermediateField 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
subalgebraEquivIntermediateField 📖	CompOp	2 math math: mem_subalgebraEquivIntermediateField, mem_subalgebraEquivIntermediateField_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_subalgebraEquivIntermediateField 📖	mathematical	—	IntermediateField SetLike.instMembership IntermediateField.instSetLike DFunLike.coe OrderIso Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder IntermediateField.instPartialOrder instFunLikeOrderIso subalgebraEquivIntermediateField Subalgebra.instSetLike	—	—
mem_subalgebraEquivIntermediateField_symm 📖	mathematical	—	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike DFunLike.coe OrderIso IntermediateField Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder Subalgebra.instPartialOrder instFunLikeOrderIso OrderIso.symm subalgebraEquivIntermediateField IntermediateField.instSetLike	—	—

---

← Back to Index