IsGaloisGroup

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

Statistics

Metric	Count
Definitions `mulSemiringAction_of_isGaloisGroup`, `IsGaloisGroup`, `intermediateFieldEquivSubgroup`, `mulEquivAlgEquiv`, `mulEquivCongr`	5
Theorems `card_eq_finrank`, `card_fixingSubgroup_eq_finrank`, `commutes`, `faithful`, `finite`, `finiteDimensional`, `finrank_fixedPoints_eq_card_subgroup`, `fixedPoints`, `fixedPoints_bot`, `fixedPoints_eq_bot`, `fixedPoints_fixingSubgroup`, `fixedPoints_le_of_le`, `fixedPoints_top`, `fixingSubgroup_bot`, `fixingSubgroup_fixedPoints`, `fixingSubgroup_le_of_le`, `fixingSubgroup_top`, `iff_isFractionRing`, `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_isFractionRing`, `of_isGalois`, `of_mulEquiv`, `of_mulEquiv_algEquiv`, `subgroup`, `toFractionRing`, `to_isFractionRing`, `instIsGaloisGroupIntRingOfIntegersOfRat`, `instIsGaloisGroupRingOfIntegersOfNumberField`	40
Total	45

FractionRing

Definitions

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

IsGaloisGroup

Definitions

Name	Category	Theorems
`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`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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`
`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` `DivisionRing.toRing` `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` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `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` `IntermediateField.instPartialOrder` `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`	—	`Subgroup.smulCommClass_left`
`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` `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.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`
`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` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `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_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`	—	`of_mulEquiv` `of_isGalois`
`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` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.instAlgebraSubtypeMem` `Algebra.id`	—	`Subgroup.smulCommClass_left` `commutes` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `faithful` `Subgroup.instFaithfulSMulSubtypeMem` `FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield`
`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	12 math math: `IsGaloisGroup.iff_isFractionRing`, `IsGaloisGroup.of_mulEquiv`, `instIsGaloisGroupIntRingOfIntegersOfRat`, `IsGaloisGroup.of_isGalois`, `IsGaloisGroup.toFractionRing`, `IsGaloisGroup.of_mulEquiv_algEquiv`, `instIsGaloisGroupRingOfIntegersOfNumberField`, `IsGaloisGroup.intermediateField`, `IsGaloisGroup.of_isFractionRing`, `IsGaloisGroup.fixedPoints`, `IsGaloisGroup.to_isFractionRing`, `IsGaloisGroup.subgroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsGaloisGroupIntRingOfIntegersOfRat` 📖	mathematical	—	`IsGaloisGroup` `NumberField.RingOfIntegers` `Int.instCommSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NumberField.RingOfIntegers.instCommRing` `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.RingOfIntegers.instCommRing` `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