Documentation Verification Report

Infinite

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

Statistics

Metric	Count
Definitions `GaloisCoinsertionIntermediateFieldSubgroup`, `GaloisInsertionIntermediateFieldClosedSubgroup`, `IntermediateFieldEquivClosedSubgroup`, `normalAutEquivQuotient`	4
Theorems `fixedField_bot`, `fixedField_fixingSubgroup`, `fixingSubgroup_fixedField`, `fixingSubgroup_isClosed`, `isOpen_and_normal_iff_finite_and_isGalois`, `isOpen_iff_finite`, `mem_bot_iff_fixed`, `mem_range_algebraMap_iff_fixed`, `normalAutEquivQuotient_apply`, `normal_iff_isGalois`, `restrict_fixedField`	11
Total	15

InfiniteGalois

Definitions

Name	Category	Theorems
`GaloisCoinsertionIntermediateFieldSubgroup` 📖	CompOp	—
`GaloisInsertionIntermediateFieldClosedSubgroup` 📖	CompOp	—
`IntermediateFieldEquivClosedSubgroup` 📖	CompOp	—
`normalAutEquivQuotient` 📖	CompOp	1 math math: `normalAutEquivQuotient_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fixedField_bot` 📖	mathematical	—	`IntermediateField.fixedField` `Top.top` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instTop` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IntermediateField.fixingSubgroup_bot` `fixedField_fixingSubgroup`
`fixedField_fixingSubgroup` 📖	mathematical	—	`IntermediateField.fixedField` `IntermediateField.fixingSubgroup`	—	`le_antisymm` `IsGalois.tower_top_intermediateField` `Finite.of_fintype` `FiniteGaloisIntermediateField.subset_adjoin` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `List.TFAE.out` `IsGalois.tfae` `FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField` `FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField` `IntermediateField.mem_fixedField_iff` `IntermediateField.isScalarTower_mid'` `IsGalois.to_normal` `AlgEquiv.restrictNormalHom_surjective` `Subtype.val_injective` `IsScalarTower.left` `AlgEquiv.restrictNormalHom_apply` `IntermediateField.mem_bot` `IntermediateField.le_iff_le` `le_rfl`
`fixingSubgroup_fixedField` 📖	mathematical	—	`IntermediateField.fixingSubgroup` `IntermediateField.fixedField` `ClosedSubgroup.toSubgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `krullTopology`	—	`le_antisymm` `IsOpen.mem_nhds` `IsClosed.isOpen_compl` `ClosedSubgroup.isClosed'` `GroupFilterBasis.nhds_eq` `Membership.mem.out` `IsScalarTower.left` `normalClosure.is_finiteDimensional` `IsGalois.normalClosure` `Set.smul_set_subset_iff` `Set.smul_mem_smul_set` `IntermediateField.fixingSubgroup_le` `IntermediateField.le_normalClosure` `mem_fixingSubgroup_iff` `IntermediateField.isScalarTower_mid'` `normalClosure.normal` `IsGalois.to_normal` `IntermediateField.fixingSubgroup_fixedField` `Subtype.val_injective` `AlgEquiv.restrictNormalHom_apply` `restrict_fixedField` `IntermediateField.mem_lift` `mul_inv_cancel_left` `inv_mul_cancel` `Set.not_subset` `IntermediateField.le_iff_le` `le_rfl`
`fixingSubgroup_isClosed` 📖	mathematical	—	`IsClosed` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `krullTopology` `SetLike.coe` `Subgroup` `AlgEquiv.aut` `Subgroup.instSetLike` `IntermediateField.fixingSubgroup`	—	`isOpen_iff_mem_nhds` `mem_nhds_iff` `Set.not_subset` `Iff.not` `mem_fixingSubgroup_iff` `Finite.of_fintype` `Set.mem_smul_set` `Mathlib.Tactic.Push.not_forall_eq` `FiniteGaloisIntermediateField.adjoin_simple_le_iff` `le_rfl` `IsOpen.smul` `IsScalarTower.continuousConstSMul` `IsScalarTower.left` `IsTopologicalGroup.toContinuousMul` `instIsTopologicalGroupAlgEquiv` `IntermediateField.fixingSubgroup_isOpen` `FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField` `mul_one`
`isOpen_and_normal_iff_finite_and_isGalois` 📖	mathematical	—	`IsOpen` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `krullTopology` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `IntermediateField.fixingSubgroup` `Subgroup.Normal` `FiniteDimensional` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `IntermediateField.toField` `IntermediateField.module'` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `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` `IsGalois` `IntermediateField.algebra'`	—	`IsScalarTower.left` `isOpen_iff_finite` `normal_iff_isGalois`
`isOpen_iff_finite` 📖	mathematical	—	`IsOpen` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `krullTopology` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Submonoid.toSubsemigroup` `Subgroup.toSubmonoid` `IntermediateField.fixingSubgroup` `FiniteDimensional` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `IntermediateField.toField` `IntermediateField.module'` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `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` `IsOpen.mem_nhds` `GroupFilterBasis.nhds_one_eq` `Membership.mem.out` `normalClosure.is_finiteDimensional` `IsGalois.normalClosure` `le_trans` `fixedField_fixingSubgroup` `IntermediateField.le_iff_le` `IntermediateField.le_normalClosure` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `FiniteDimensional.left` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `IsScalarTower.of_algHom` `SubsemiringClass.nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.fixingSubgroup_isOpen`
`mem_bot_iff_fixed` 📖	mathematical	—	`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` `DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike`	—	—
`mem_range_algebraMap_iff_fixed` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `AlgEquiv` `AlgEquiv.instFunLike`	—	`mem_bot_iff_fixed`
`normalAutEquivQuotient_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `QuotientGroup.instHasQuotientSubgroup` `ClosedSubgroup.toSubgroup` `krullTopology` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.fixedField` `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` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `normalAutEquivQuotient` `MonoidHom` `MonoidHom.instFunLike` `AlgEquiv.restrictNormalHom` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `IsGalois.to_normal` `IsGalois.of_fixedField_normal_subgroup`	—	`IsScalarTower.left`
`normal_iff_isGalois` 📖	mathematical	—	`Subgroup.Normal` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `IntermediateField.fixingSubgroup` `IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `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`	—	`IsScalarTower.left` `Finite.of_fintype` `IntermediateField.isScalarTower_mid'` `IsGalois.to_normal` `FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField` `Subgroup.Normal.map` `AlgEquiv.restrictNormalHom_surjective` `Normal.of_algEquiv` `IntermediateField.isScalarTower` `IsGalois.of_fixedField_normal_subgroup` `IntermediateField.normal_iSup` `le_antisymm` `iSup_le` `restrict_fixedField` `fixedField_fixingSubgroup` `inf_le_left` `le_iSup` `FiniteGaloisIntermediateField.adjoin_simple_le_iff` `le_rfl` `IntermediateField.isSeparable_tower_bot` `IsGalois.to_isSeparable` `IntermediateField.restrictNormalHom_ker` `MonoidHom.normal_ker`
`restrict_fixedField` 📖	mathematical	—	`IntermediateField` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `IntermediateField.fixedField` `IntermediateField.lift` `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` `Field.toCommRing` `Module.toDistribMulAction` `Algebra.toModule` `Subgroup.map` `AlgEquiv` `AlgEquiv.aut` `AlgEquiv.restrictNormalHom` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'`	—	`IsScalarTower.left` `SetLike.ext'` `IntermediateField.isScalarTower_mid'` `Set.ext` `Membership.mem.out` `IntermediateField.mem_lift` `Subtype.val_injective` `AlgEquiv.restrictNormal_commutes` `IntermediateField.lift_le`

---

← Back to Index