Abelian

📁 Source: Mathlib/FieldTheory/Galois/Abelian.lean

Statistics

Metric	Count
Definitions IsAbelianGalois	1
Theorems of_algHom, of_isCyclic, toIsGalois, toIsMulCommutative, tower_bot, tower_top, instIsAbelianGalois, instIsAbelianGaloisSubtypeMemIntermediateField, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, instIsAbelianGaloisSubtypeMemIntermediateField_1	10
Total	11

IsAbelianGalois

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_algHom 📖	mathematical	—	IsAbelianGalois	—	tower_bot IsScalarTower.of_algebraMap_eq' AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap
of_isCyclic 📖	mathematical	—	IsAbelianGalois	—	IsCyclic.commutative
toIsGalois 📖	mathematical	—	IsGalois	—	—
toIsMulCommutative 📖	mathematical	—	IsMulCommutative AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut	—	—
tower_bot 📖	mathematical	—	IsAbelianGalois	—	AlgEquiv.transfer_galois RingHom.injective DivisionRing.isSimpleRing SubsemiringClass.nontrivial Subalgebra.instSubsemiringClass IsLocalRing.toNontrivial Field.instIsLocalRing AlgHom.rangeRestrict_surjective IsScalarTower.left InfiniteGalois.normal_iff_isGalois toIsGalois Subgroup.normal_of_comm toIsMulCommutative IsGalois.to_normal AlgEquiv.restrictNormalHom_surjective map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mul_comm
tower_top 📖	mathematical	—	IsAbelianGalois	—	IsGalois.tower_top_of_isGalois toIsGalois AlgEquiv.restrictScalars_injective mul_comm toIsMulCommutative

(root)

Definitions

Name	Category	Theorems
IsAbelianGalois 📖	CompData	9 math math: instIsAbelianGaloisSubtypeMemIntermediateFieldBot, instIsAbelianGalois, instIsAbelianGaloisSubtypeMemIntermediateField_1, IsCyclotomicExtension.isAbelianGalois, IsAbelianGalois.tower_top, IsAbelianGalois.of_algHom, IsAbelianGalois.tower_bot, instIsAbelianGaloisSubtypeMemIntermediateField, IsAbelianGalois.of_isCyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAbelianGalois 📖	mathematical	—	IsAbelianGalois Algebra.id Semifield.toCommSemiring Field.toSemifield	—	IsGalois.self AlgEquiv.subsingleton_right Unique.instSubsingleton
instIsAbelianGaloisSubtypeMemIntermediateField 📖	mathematical	—	IsAbelianGalois IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField IntermediateField.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	—	IsAbelianGalois.tower_bot IsScalarTower.left IntermediateField.isScalarTower_mid'
instIsAbelianGaloisSubtypeMemIntermediateFieldBot 📖	mathematical	—	IsAbelianGalois IntermediateField SetLike.instMembership IntermediateField.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder IntermediateField.toField IntermediateField.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	—	IsAbelianGalois.of_algHom IsScalarTower.left instIsAbelianGalois
instIsAbelianGaloisSubtypeMemIntermediateField_1 📖	mathematical	—	IsAbelianGalois IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField IntermediateField.instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring	—	IsAbelianGalois.tower_top IsScalarTower.left IntermediateField.isScalarTower_mid'

---

← Back to Index