Documentation Verification Report

HilbertTheory

📁 Source: Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

Statistics

Metric	Count
Definitions `IsDecompositionField`, `ringEquiv`, `IsInertiaField`, `ringEquiv`	4
Theorems `algebraMap_ringEquiv_apply`, `algebraMap_ringEquiv_symm_apply`, `of_isGaloisGroup`, `rank_left`, `rank_right`, `toIsGaloisGroup`, `algebraMap_ringEquiv_apply`, `algebraMap_ringEquiv_symm_apply`, `of_isGaloisGroup`, `rank_decompositionField`, `rank_left`, `rank_right`, `toIsGaloisGroup`, `instIsDecompositionFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupStabilizerIdeal`, `instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois`, `instIsInertiaFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupInertia`, `instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois`, `isDecompositionField_iff`, `isInertiaField_iff`	19
Total	23

IsDecompositionField

Definitions

Name	Category	Theorems
`ringEquiv` 📖	CompOp	2 math math: `algebraMap_ringEquiv_symm_apply`, `algebraMap_ringEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_ringEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `ringEquiv`	—	`IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply` `toIsGaloisGroup`
`algebraMap_ringEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `ringEquiv`	—	`IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply` `toIsGaloisGroup`
`of_isGaloisGroup` 📖	mathematical	—	`IsDecompositionField`	—	`isDecompositionField_iff` `IsGaloisGroup.of_mulEquiv` `FaithfulSMul.algebraMap_injective` `IsFractionRing.instFaithfulSMul` `algebraMap.smul'` `IsFractionRing.div_surjective` `smul_div₀'` `Ideal.stabilizerEquiv_symm_apply_smul`
`rank_left` 📖	mathematical	—	`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` `Ideal.ramificationIdxIn` `Ideal.inertiaDegIn`	—	`Ideal.IsMaximal.under` `Algebra.IsIntegral.of_finite` `Ideal.over_def` `Ring.HasFiniteQuotients.finiteQuotient` `IsGaloisGroup.card_eq_finrank` `toIsGaloisGroup` `Ideal.card_stabilizer_eq` `Finite.algEquiv` `Finite.algHom` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `module_finite_of_liesOver` `PerfectField.ofFinite`
`rank_right` 📖	mathematical	—	`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` `Set.ncard` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.primesOver`	—	`Ideal.IsMaximal.under` `Algebra.IsIntegral.of_finite` `Ideal.over_def` `FiniteDimensional.right` `mul_left_injective₀` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Module.finrank_mul_finrank` `Module.Free.of_divisionRing` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `rank_left` `Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn` `Finite.algEquiv` `Finite.algHom` `IsGaloisGroup.card_eq_finrank` `IsGaloisGroup.of_isGalois`
`toIsGaloisGroup` 📖	mathematical	—	`IsGaloisGroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `Ideal.pointwiseDistribMulAction` `Subgroup.toGroup` `Subgroup.mulSemiringAction` `AlgEquiv.applyMulSemiringAction`	—	—

IsInertiaField

Definitions

Name	Category	Theorems
`ringEquiv` 📖	CompOp	2 math math: `algebraMap_ringEquiv_apply`, `algebraMap_ringEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_ringEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `ringEquiv`	—	`IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply` `toIsGaloisGroup`
`algebraMap_ringEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `ringEquiv`	—	`IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply` `toIsGaloisGroup`
`of_isGaloisGroup` 📖	mathematical	—	`IsInertiaField`	—	`isInertiaField_iff` `IsGaloisGroup.of_mulEquiv` `FaithfulSMul.algebraMap_injective` `IsFractionRing.instFaithfulSMul` `algebraMap.smul'` `IsFractionRing.div_surjective` `smul_div₀'` `Ideal.inertiaEquiv_symm_apply_smul`
`rank_decompositionField` 📖	mathematical	—	`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` `Ideal.inertiaDegIn`	—	`Ideal.IsMaximal.under` `Algebra.IsIntegral.of_finite` `Ideal.over_def` `Module.finrank_mul_finrank` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `primesOver_ncard_ne_zero` `IsDedekindDomain.toIsDomain` `IsDecompositionField.rank_right` `rank_right`
`rank_left` 📖	mathematical	—	`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` `Ideal.ramificationIdxIn`	—	`Ideal.IsMaximal.under` `Algebra.IsIntegral.of_finite` `Ideal.over_def` `Ring.HasFiniteQuotients.finiteQuotient` `IsGaloisGroup.card_eq_finrank` `toIsGaloisGroup` `Ideal.card_inertia_eq_ramificationIdxIn` `Finite.algEquiv` `Finite.algHom` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `module_finite_of_liesOver` `PerfectField.ofFinite`
`rank_right` 📖	mathematical	—	`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` `Set.ncard` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.primesOver` `Ideal.inertiaDegIn`	—	`Ideal.IsMaximal.under` `Algebra.IsIntegral.of_finite` `Ideal.over_def` `FiniteDimensional.right` `mul_left_injective₀` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Module.finrank_mul_finrank` `Module.Free.of_divisionRing` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `rank_left` `mul_assoc` `mul_comm` `Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn` `Finite.algEquiv` `Finite.algHom` `IsGaloisGroup.card_eq_finrank` `IsGaloisGroup.of_isGalois`
`toIsGaloisGroup` 📖	mathematical	—	`IsGaloisGroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `Ideal.inertia` `CommRing.toRing` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulSemiringAction.toDistribMulAction` `Subgroup.toGroup` `Subgroup.mulSemiringAction` `AlgEquiv.applyMulSemiringAction`	—	—

(root)

Definitions

Name	Category	Theorems
`IsDecompositionField` 📖	CompData	4 math math: `isDecompositionField_iff`, `IsDecompositionField.of_isGaloisGroup`, `instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois`, `instIsDecompositionFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupStabilizerIdeal`
`IsInertiaField` 📖	CompData	4 math math: `IsInertiaField.of_isGaloisGroup`, `isInertiaField_iff`, `instIsInertiaFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupInertia`, `instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDecompositionFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupStabilizerIdeal` 📖	mathematical	—	`IsDecompositionField`	—	—
`instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois` 📖	mathematical	—	`IsDecompositionField` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `FixedPoints.intermediateField` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `Subgroup.instSetLike` `MulAction.stabilizer` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `Ideal.pointwiseDistribMulAction` `Subgroup.toGroup` `Subgroup.mulSemiringAction` `AlgEquiv.applyMulSemiringAction` `Subgroup.smulCommClass_left` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulSemiringAction.toDistribMulAction` `Algebra.toSMul` `AlgEquiv.apply_smulCommClass'` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem`	—	`Subgroup.smulCommClass_left` `AlgEquiv.apply_smulCommClass'` `IsScalarTower.left` `IsGaloisGroup.subgroup` `IsGaloisGroup.of_isGalois`
`instIsInertiaFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupInertia` 📖	mathematical	—	`IsInertiaField`	—	—
`instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois` 📖	mathematical	—	`IsInertiaField` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `FixedPoints.intermediateField` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `Subgroup.instSetLike` `Ideal.inertia` `CommRing.toRing` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulSemiringAction.toDistribMulAction` `Subgroup.toGroup` `Subgroup.mulSemiringAction` `AlgEquiv.applyMulSemiringAction` `Subgroup.smulCommClass_left` `Algebra.toSMul` `AlgEquiv.apply_smulCommClass'` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem`	—	`Subgroup.smulCommClass_left` `AlgEquiv.apply_smulCommClass'` `IsScalarTower.left` `IsGaloisGroup.subgroup` `IsGaloisGroup.of_isGalois`
`isDecompositionField_iff` 📖	mathematical	—	`IsDecompositionField` `IsGaloisGroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `Ideal.pointwiseDistribMulAction` `Subgroup.toGroup` `Subgroup.mulSemiringAction` `AlgEquiv.applyMulSemiringAction`	—	—
`isInertiaField_iff` 📖	mathematical	—	`IsInertiaField` `IsGaloisGroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `Ideal.inertia` `CommRing.toRing` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulSemiringAction.toDistribMulAction` `Subgroup.toGroup` `Subgroup.mulSemiringAction` `AlgEquiv.applyMulSemiringAction`	—	—

---

← Back to Index