IsGaloisGroup

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

Statistics

Metric	Count
Definitions mulSemiringAction_of_isGaloisGroup, IsGaloisGroup, instMulSemiringActionQuotientSubgroupSubtypeMemIntermediateField, instSMulQuotientSubgroupSubtypeMemIntermediateField, intermediateFieldEquivSubgroup, mulEquivAlgEquiv, mulEquivCongr, ringEquiv, ringEquivFixedPoints	9
Theorems algebraMap_ringEquivFixedPoints_symm_apply, algebraMap_ringEquiv_apply, algebraMap_ringEquiv_symm_apply, card_eq_finrank, card_fixingSubgroup_eq_finrank, coe_quotient_smul, commutes, faithful, finite, finiteDimensional, finrank_fixedPoints_eq_card_subgroup, fixedPoints, fixedPoints_bot, fixedPoints_eq_bot, fixedPoints_fixingSubgroup, fixedPoints_le_of_le, fixedPoints_of_isGaloisGroup, fixedPoints_top, fixingSubgroup_bot, fixingSubgroup_fixedPoints, fixingSubgroup_le_of_le, fixingSubgroup_top, iff_isFractionRing, instSMulCommClassQuotientSubgroupSubtypeMemIntermediateField, intermediateField, intermediateFieldEquivSubgroup_apply, intermediateFieldEquivSubgroup_symm_apply, intermediateFieldEquivSubgroup_symm_apply_toDual, isGalois, isInvariant, le_fixedPoints_iff_le_fixingSubgroup, map_mulEquivAlgEquiv_fixingSubgroup, mulEquivAlgEquiv_apply_apply, mulEquivAlgEquiv_apply_symm_apply, mulEquivAlgEquiv_symm_apply, mulEquivCongr_apply_smul, ofDual_intermediateFieldEquivSubgroup_apply, of_fixedPoints_eq, of_isFractionRing, of_isGalois, of_mulEquiv, of_mulEquiv_algEquiv, quotient, quotientMap, ringEquivFixedPoints_apply_coe, smul_eq_self, smul_mem_of_normal, subgroup, subgroup_iff, toFractionRing, to_isFractionRing, instIsGaloisGroupIntRingOfIntegersOfRat, instIsGaloisGroupRingOfIntegersOfNumberField	53
Total	62

FractionRing

Definitions

Name	Category	Theorems
mulSemiringAction_of_isGaloisGroup 📖	CompOp	1 math math: IsGaloisGroup.toFractionRing

IsGaloisGroup

Definitions

Name	Category	Theorems
instMulSemiringActionQuotientSubgroupSubtypeMemIntermediateField 📖	CompOp	2 math math: quotientMap, quotient
instSMulQuotientSubgroupSubtypeMemIntermediateField 📖	CompOp	2 math math: instSMulCommClassQuotientSubgroupSubtypeMemIntermediateField, coe_quotient_smul
intermediateFieldEquivSubgroup 📖	CompOp	4 math math: ofDual_intermediateFieldEquivSubgroup_apply, intermediateFieldEquivSubgroup_symm_apply, intermediateFieldEquivSubgroup_apply, intermediateFieldEquivSubgroup_symm_apply_toDual
mulEquivAlgEquiv 📖	CompOp	4 math math: mulEquivAlgEquiv_apply_symm_apply, mulEquivAlgEquiv_apply_apply, mulEquivAlgEquiv_symm_apply, map_mulEquivAlgEquiv_fixingSubgroup
mulEquivCongr 📖	CompOp	1 math math: mulEquivCongr_apply_smul
ringEquiv 📖	CompOp	2 math math: algebraMap_ringEquiv_symm_apply, algebraMap_ringEquiv_apply
ringEquivFixedPoints 📖	CompOp	2 math math: algebraMap_ringEquivFixedPoints_symm_apply, ringEquivFixedPoints_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_ringEquivFixedPoints_symm_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap RingEquiv Subsemiring SetLike.instMembership Subsemiring.instSetLike FixedPoints.subsemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Subsemiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm ringEquivFixedPoints	—	Algebra.IsInvariant.isInvariant isInvariant Subtype.prop
algebraMap_ringEquiv_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquiv	—	algebraMap_ringEquivFixedPoints_symm_apply
algebraMap_ringEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm ringEquiv	—	algebraMap_ringEquivFixedPoints_symm_apply
card_eq_finrank 📖	mathematical	—	Nat.card Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	—	faithful IntermediateField.finrank_bot' commutes fixedPoints_eq_bot Nat.card_eq_fintype_card FixedPoints.finrank_eq_card Nat.card_eq_zero_of_infinite Mathlib.Tactic.Contrapose.contrapose₁ FiniteDimensional.of_finrank_pos Finite.of_injective Finite.algEquiv Finite.algHom Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors FaithfulSMul.eq_of_smul_eq_smul DFunLike.ext_iff
card_fixingSubgroup_eq_finrank 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField IntermediateField.instSetLike Module.finrank IntermediateField.toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.instModuleSubtypeMem Semiring.toModule	—	card_eq_finrank intermediateField
coe_quotient_smul 📖	mathematical	—	IntermediateField SetLike.instMembership IntermediateField.instSetLike HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup instSMulQuotientSubgroupSubtypeMemIntermediateField SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass
commutes 📖	mathematical	—	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Algebra.toSMul	—	—
faithful 📖	mathematical	—	FaithfulSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction	—	—
finite 📖	mathematical	—	Finite	—	Nat.finite_of_card_ne_zero LT.lt.ne' Module.finrank_pos commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors card_eq_finrank
finiteDimensional 📖	mathematical	—	FiniteDimensional Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing Algebra.toModule Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	FiniteDimensional.of_finrank_pos Nat.card_pos One.instNonempty card_eq_finrank
finrank_fixedPoints_eq_card_subgroup 📖	mathematical	—	Module.finrank IntermediateField SetLike.instMembership IntermediateField.instSetLike FixedPoints.intermediateField Subgroup Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring commutes IntermediateField.toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.instModuleSubtypeMem Semiring.toModule Nat.card	—	Subgroup.smulCommClass_left commutes card_eq_finrank subgroup
fixedPoints 📖	mathematical	—	IsGaloisGroup Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike FixedPoints.subfield DivInvMonoid.toMonoid Group.toDivInvMonoid SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring FixedPoints.instAlgebraSubtypeMemSubfieldSubfield	—	of_mulEquiv_algEquiv IsGalois.of_fixed_field
fixedPoints_bot 📖	mathematical	—	FixedPoints.intermediateField Subgroup SetLike.instMembership Subgroup.instSetLike Bot.bot Subgroup.instBot DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Subgroup.smulCommClass_left one_smul
fixedPoints_eq_bot 📖	mathematical	—	FixedPoints.intermediateField DivInvMonoid.toMonoid Group.toDivInvMonoid commutes Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Bot.bot IntermediateField OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	commutes eq_bot_iff Algebra.IsInvariant.isInvariant isInvariant
fixedPoints_fixingSubgroup 📖	mathematical	—	FixedPoints.intermediateField Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField IntermediateField.instSetLike Subgroup.toGroup Subgroup.mulSemiringAction Subgroup.smulCommClass_left Algebra.toSMul Semifield.toCommSemiring commutes	—	Subgroup.smulCommClass_left commutes ofDual_intermediateFieldEquivSubgroup_apply intermediateFieldEquivSubgroup_symm_apply OrderIso.symm_apply_apply
fixedPoints_le_of_le 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	IntermediateField Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder FixedPoints.intermediateField Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring	—	Subgroup.smulCommClass_left
fixedPoints_of_isGaloisGroup 📖	mathematical	—	FixedPoints.intermediateField Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring commutes	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass Subgroup.smulCommClass_left commutes IntermediateField.ext_iff Algebra.IsInvariant.isInvariant isInvariant Subtype.prop IsScalarTower.left IntermediateField.isScalarTower_mid' fixedPoints_eq_bot IntermediateField.restrictScalars_bot_eq_self
fixedPoints_top 📖	mathematical	—	FixedPoints.intermediateField Subgroup SetLike.instMembership Subgroup.instSetLike Top.top Subgroup.instTop DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring commutes Bot.bot IntermediateField OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Subgroup.smulCommClass_left commutes IntermediateField.ext fixedPoints_eq_bot
fixingSubgroup_bot 📖	mathematical	—	fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField IntermediateField.instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Top.top Subgroup Subgroup.instTop	—	smul_algebraMap
fixingSubgroup_fixedPoints 📖	mathematical	—	fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField IntermediateField.instSetLike FixedPoints.intermediateField Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.mulSemiringAction Subgroup.smulCommClass_left Algebra.toSMul Semifield.toCommSemiring commutes	—	Subgroup.smulCommClass_left commutes intermediateFieldEquivSubgroup_symm_apply_toDual ofDual_intermediateFieldEquivSubgroup_apply OrderIso.apply_symm_apply OrderDual.ofDual_toDual
fixingSubgroup_le_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField IntermediateField.instSetLike	—	—
fixingSubgroup_top 📖	mathematical	—	fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField IntermediateField.instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Bot.bot Subgroup Subgroup.instBot	—	faithful Subgroup.ext MulAction.fixedBy_eq_univ_iff_eq_one
iff_isFractionRing 📖	mathematical	—	IsGaloisGroup CommRing.toCommSemiring CommSemiring.toSemiring Algebra.IsIntegral CommRing.toRing Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Algebra.IsInvariant.isIntegral isInvariant to_isFractionRing of_isFractionRing
instSMulCommClassQuotientSubgroupSubtypeMemIntermediateField 📖	mathematical	—	SMulCommClass HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup IntermediateField SetLike.instMembership IntermediateField.instSetLike instSMulQuotientSubgroupSubtypeMemIntermediateField Algebra.toSMul Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' CommSemiring.toSemiring Algebra.id 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 Algebra.toModule	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.left Quotient.inductionOn' SMulCommClass.smul_comm
intermediateField 📖	mathematical	—	IsGaloisGroup Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField IntermediateField.instSetLike Subgroup.toGroup SubsemiringClass.toCommSemiring Semifield.toCommSemiring SubringClass.toSubsemiringClass NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SubfieldClass.toSubringClass Field.toDivisionRing IntermediateField.instSubfieldClass IntermediateField.instAlgebraSubtypeMem Algebra.id Subgroup.mulSemiringAction	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass map_mulEquivAlgEquiv_fixingSubgroup isGalois of_mulEquiv_algEquiv IsGalois.tower_top_intermediateField
intermediateFieldEquivSubgroup_apply 📖	mathematical	—	DFunLike.coe OrderIso IntermediateField OrderDual Subgroup Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder OrderDual.instLE Subgroup.instPartialOrder instFunLikeOrderIso intermediateFieldEquivSubgroup Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField.instSetLike	—	—
intermediateFieldEquivSubgroup_symm_apply 📖	mathematical	—	DFunLike.coe OrderIso OrderDual Subgroup IntermediateField OrderDual.instLE Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder IntermediateField.instPartialOrder instFunLikeOrderIso OrderIso.symm intermediateFieldEquivSubgroup FixedPoints.intermediateField SetLike.instMembership Subgroup.instSetLike Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring commutes	—	Subgroup.smulCommClass_left commutes Equiv.surjective Function.Surjective.forall MulEquiv.surjective MulEquiv.symm_apply_apply
intermediateFieldEquivSubgroup_symm_apply_toDual 📖	mathematical	—	DFunLike.coe OrderIso OrderDual Subgroup IntermediateField OrderDual.instLE Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder IntermediateField.instPartialOrder instFunLikeOrderIso OrderIso.symm intermediateFieldEquivSubgroup Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual FixedPoints.intermediateField SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring commutes	—	intermediateFieldEquivSubgroup_symm_apply
isGalois 📖	mathematical	—	IsGalois	—	isGalois_iff_isGalois_bot commutes fixedPoints_eq_bot IsGalois.of_fixed_field
isInvariant 📖	mathematical	—	Algebra.IsInvariant	—	—
le_fixedPoints_iff_le_fixingSubgroup 📖	mathematical	—	IntermediateField Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder FixedPoints.intermediateField Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Subgroup.instPartialOrder fixingSubgroup SetLike.coe IntermediateField.instSetLike	—	Subgroup.smulCommClass_left
map_mulEquivAlgEquiv_fixingSubgroup 📖	mathematical	—	Subgroup.map AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.aut MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass mulEquivAlgEquiv fixingSubgroup DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField IntermediateField.instSetLike IntermediateField.fixingSubgroup	—	Subgroup.ext MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass MulEquiv.surjective EquivLike.toEmbeddingLike
mulEquivAlgEquiv_apply_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike mulEquivAlgEquiv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	—
mulEquivAlgEquiv_apply_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike AlgEquiv.symm MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike mulEquivAlgEquiv SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mulEquivAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm mulEquivAlgEquiv Function.surjInv MonoidHom MonoidHom.instFunLike MulSemiringAction.toAlgAut Function.Bijective.surjective	—	—
mulEquivCongr_apply_smul 📖	mathematical	—	SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike mulEquivCongr	—	AlgEquiv.ext_iff MulEquiv.apply_symm_apply
ofDual_intermediateFieldEquivSubgroup_apply 📖	mathematical	—	DFunLike.coe Equiv OrderDual Subgroup EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderIso IntermediateField Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder OrderDual.instLE Subgroup.instPartialOrder instFunLikeOrderIso intermediateFieldEquivSubgroup fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulSemiringAction.toDistribMulAction SetLike.coe IntermediateField.instSetLike	—	—
of_fixedPoints_eq 📖	mathematical	FixedPoints.intermediateField Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring commutes	IsGaloisGroup Subgroup SetLike.instMembership Subgroup.instSetLike IntermediateField IntermediateField.instSetLike Subgroup.toGroup SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SubfieldClass.toSubringClass Field.toDivisionRing IntermediateField.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.instAlgebraSubtypeMem Algebra.id Subgroup.mulSemiringAction	—	Subgroup.smulCommClass_left commutes SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass subgroup
of_isFractionRing 📖	mathematical	—	IsGaloisGroup CommRing.toCommSemiring CommSemiring.toSemiring	—	faithful FaithfulSMul.eq_of_smul_eq_smul IsFractionRing.div_surjective smul_div₀' IsFractionRing.injective Algebra.smul_def smul_mul' map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass algebraMap.coe_smul' smul_algebraMap commutes Algebra.IsInvariant.isInvariant isInvariant IsFractionRing.instFaithfulSMul IsIntegral.algebraMap Algebra.IsIntegral.isIntegral IsIntegrallyClosedIn.isIntegral_iff IsIntegralClosure.of_isIntegrallyClosed IsScalarTower.left IsPurelyInseparable.isIntegral isPurelyInseparable_self isIntegral_algebraMap_iff RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing
of_isGalois 📖	mathematical	—	IsGaloisGroup AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.aut AlgEquiv.applyMulSemiringAction	—	AlgEquiv.apply_faithfulSMul AlgEquiv.apply_smulCommClass' IsScalarTower.left InfiniteGalois.mem_bot_iff_fixed
of_mulEquiv 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike	IsGaloisGroup	—	MulEquiv.injective FaithfulSMul.eq_of_smul_eq_smul faithful SMulCommClass.smul_comm commutes MulEquiv.apply_symm_apply Algebra.IsInvariant.isInvariant isInvariant
of_mulEquiv_algEquiv 📖	mathematical	DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero instSMulZeroClass MulSemiringAction.toMulDistribMulAction	IsGaloisGroup Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	of_mulEquiv of_isGalois
quotient 📖	mathematical	—	IsGaloisGroup HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup IntermediateField SetLike.instMembership IntermediateField.instSetLike QuotientGroup.Quotient.group Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id 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 Algebra.toModule instMulSemiringActionQuotientSubgroupSubtypeMemIntermediateField	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.left Quotient.inductionOn₂' QuotientGroup.eq Subgroup.smulCommClass_left commutes fixingSubgroup_fixedPoints subgroup_iff mem_fixingSubgroup_iff SemigroupAction.mul_smul inv_smul_eq_iff instSMulCommClassQuotientSubgroupSubtypeMemIntermediateField Algebra.IsInvariant.isInvariant isInvariant FaithfulSMul.algebraMap_injective IntermediateField.instFaithfulSMulSubtypeMem Module.Free.instFaithfulSMulOfNontrivial Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsDomain Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing IsScalarTower.algebraMap_apply IntermediateField.isScalarTower_mid' IntermediateField.algebraMap_apply
quotientMap 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder	IsGaloisGroup HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group SetLike.instMembership Subgroup.instSetLike Subgroup.map QuotientGroup.mk' IntermediateField IntermediateField.instSetLike Subgroup.toGroup SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SubfieldClass.toSubringClass Field.toDivisionRing IntermediateField.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField RingHom.toAlgebra AlgHom.toRingHom IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule IntermediateField.inclusion Subgroup.mulSemiringAction instMulSemiringActionQuotientSubgroupSubtypeMemIntermediateField	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.left quotient faithful Subgroup.instFaithfulSMulSubtypeMem FaithfulSMul.algebraMap_injective IntermediateField.instFaithfulSMulSubtypeMem Module.Free.instFaithfulSMulOfNontrivial Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsDomain Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing SMulCommClass.smul_comm commutes Algebra.IsInvariant.isInvariant isInvariant IsScalarTower.of_algebraMap_eq' IsScalarTower.algebraMap_apply IntermediateField.algebraMap_apply
ringEquivFixedPoints_apply_coe 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership Subsemiring.instSetLike FixedPoints.subsemiring DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring Subsemiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquivFixedPoints RingHom RingHom.instFunLike algebraMap	—	—
smul_eq_self 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike	SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring IntermediateField SetLike.instMembership IntermediateField.instSetLike	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass smul_algebraMap commutes
smul_mem_of_normal 📖	mathematical	—	IntermediateField SetLike.instMembership IntermediateField.instSetLike SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass smul_assoc Subgroup.instIsScalarTowerSubtypeMem IsScalarTower.left MulAction.subgroup_smul_def smul_eq_mul add_neg_cancel zpow_zero one_mul smul_eq_self Subgroup.Normal.conj_mem' Subtype.prop Algebra.IsInvariant.isInvariant isInvariant
subgroup 📖	mathematical	—	IsGaloisGroup Subgroup SetLike.instMembership Subgroup.instSetLike IntermediateField IntermediateField.instSetLike FixedPoints.intermediateField DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring commutes SubsemiringClass.toCommSemiring SubringClass.toSubsemiringClass NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SubfieldClass.toSubringClass Field.toDivisionRing IntermediateField.instSubfieldClass IntermediateField.instAlgebraSubtypeMem Algebra.id	—	Subgroup.smulCommClass_left commutes SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass faithful Subgroup.instFaithfulSMulSubtypeMem
subgroup_iff 📖	mathematical	—	IsGaloisGroup Subgroup SetLike.instMembership Subgroup.instSetLike IntermediateField IntermediateField.instSetLike Subgroup.toGroup SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain SubfieldClass.toSubringClass Field.toDivisionRing IntermediateField.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.instAlgebraSubtypeMem Algebra.id Subgroup.mulSemiringAction FixedPoints.intermediateField DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul commutes	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass Subgroup.smulCommClass_left commutes fixedPoints_of_isGaloisGroup of_fixedPoints_eq
toFractionRing 📖	mathematical	—	IsGaloisGroup FractionRing OreLocalization.instCommSemiring CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instSemiring FractionRing.liftAlgebra FractionRing.field OreLocalization.instAlgebra FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul CommRing.toRing IsDomain.toIsCancelMulZero IsDomain.toNontrivial FractionRing.mulSemiringAction_of_isGaloisGroup	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors IsScalarTower.right Algebra.smul_def' smul_mul' IsFractionRing.fieldEquivOfAlgEquiv_algebraMap Localization.isLocalization OreLocalization.instIsScalarTower FractionRing.instIsScalarTower IsScalarTower.left to_isFractionRing FractionRing.instFaithfulSMul Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero
to_isFractionRing 📖	mathematical	—	IsGaloisGroup Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	faithful FaithfulSMul.eq_of_smul_eq_smul IsFractionRing.instFaithfulSMul IsFractionRing.div_surjective Algebra.smul_def map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass smul_mul' smul_div₀' smul_algebraMap commutes Algebra.IsInvariant.isIntegral isInvariant IsFractionRing.nontrivial_iff_nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing nonZeroDivisors.ne_zero IsAlgebraic.exists_smul_eq_mul Algebra.IsAlgebraic.isAlgebraic Algebra.IsIntegral.isAlgebraic div_eq_div_iff map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_comm Algebra.IsInvariant.isInvariant

(root)

Definitions

Name	Category	Theorems
IsGaloisGroup 📖	CompData	20 math math: IsGaloisGroup.iff_isFractionRing, IsGaloisGroup.quotientMap, IsGaloisGroup.of_mulEquiv, instIsGaloisGroupIntRingOfIntegersOfRat, IsGaloisGroup.of_fixedPoints_eq, IsDecompositionField.toIsGaloisGroup, IsGaloisGroup.quotient, isInertiaField_iff, isDecompositionField_iff, IsGaloisGroup.of_isGalois, IsGaloisGroup.toFractionRing, IsGaloisGroup.of_mulEquiv_algEquiv, instIsGaloisGroupRingOfIntegersOfNumberField, IsGaloisGroup.subgroup_iff, IsGaloisGroup.intermediateField, IsGaloisGroup.of_isFractionRing, IsGaloisGroup.fixedPoints, IsGaloisGroup.to_isFractionRing, IsGaloisGroup.subgroup, IsInertiaField.toIsGaloisGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsGaloisGroupIntRingOfIntegersOfRat 📖	mathematical	—	IsGaloisGroup NumberField.RingOfIntegers Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers Ring.toIntAlgebra CommRing.toRing NumberField.RingOfIntegers.instMulSemiringAction	—	NumberField.to_charZero IsGaloisGroup.of_isFractionRing Rat.isFractionRing NumberField.RingOfIntegers.instIsFractionRing AddCommGroup.intIsScalarTower NumberField.RingOfIntegers.instSMulDistribClass IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain Int.instIsDomain EuclideanDomain.to_principal_ideal_domain NumberField.RingOfIntegers.instIsIntegralInt
instIsGaloisGroupRingOfIntegersOfNumberField 📖	mathematical	—	IsGaloisGroup NumberField.RingOfIntegers CommRing.toCommSemiring NumberField.instCommRingRingOfIntegers CommSemiring.toSemiring NumberField.inst_ringOfIntegersAlgebra NumberField.RingOfIntegers.instMulSemiringAction	—	IsGaloisGroup.of_isFractionRing NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instIsScalarTower NumberField.RingOfIntegers.instIsScalarTower_1 NumberField.RingOfIntegers.instSMulDistribClass NumberField.RingOfIntegers.instIsIntegrallyClosed NumberField.RingOfIntegers.extension_algebra_isIntegral

---

← Back to Index