Documentation Verification Report

Basic

📁 Source: Mathlib/FieldTheory/Normal/Basic.lean

Statistics

Metric	Count
Definitions `liftNormal`, `liftNormal`	2
Theorems `liftNormal_commutes`, `restrictNormalHom_surjective`, `restrict_liftNormal`, `fieldRange_of_normal`, `liftNormal_commutes`, `restrict_liftNormal`, `normal`, `normal_iInf`, `normal_iSup`, `normal_inf`, `normal_sup`, `splits_of_mem_adjoin`, `exists_isSplittingField`, `minpoly_eq_iff_mem_orbit`, `of_isSplittingField`, `instNormal`, `isSolvable_of_isScalarTower`, `exists_algEquiv_of_root`, `exists_algEquiv_of_root'`	19
Total	21

AlgEquiv

Definitions

Name	Category	Theorems
`liftNormal` 📖	CompOp	3 math math: `restrict_liftNormal`, `InfiniteGalois.toAlgEquivAux_eq_liftNormal`, `liftNormal_commutes`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liftNormal_commutes` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instFunLike` `liftNormal` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`AlgHom.liftNormal_commutes`
`restrictNormalHom_surjective` 📖	mathematical	—	`AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `aut` `MonoidHom.instFunLike` `restrictNormalHom`	—	`restrict_liftNormal`
`restrict_liftNormal` 📖	mathematical	—	`restrictNormal` `liftNormal`	—	`ext` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `restrictNormal_commutes` `liftNormal_commutes`

AlgHom

Definitions

Name	Category	Theorems
`liftNormal` 📖	CompOp	2 math math: `liftNormal_commutes`, `restrict_liftNormal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fieldRange_of_normal` 📖	mathematical	—	`fieldRange` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `IsScalarTower.right` `IntermediateField.isScalarTower_mid'` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `DFunLike.ext_iff` `restrictNormal_commutes` `map_fieldRange` `AlgEquiv.fieldRange_eq_top` `fieldRange_eq_map` `IntermediateField.fieldRange_val`
`liftNormal_commutes` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `funLike` `liftNormal` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`commutes`
`restrict_liftNormal` 📖	mathematical	—	`restrictNormal` `liftNormal`	—	`ext` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `restrictNormal_commutes` `liftNormal_commutes`

Algebra.IsQuadraticExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normal` 📖	mathematical	—	`Normal`	—	`commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsAlgebraic.of_finite` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Algebra.instFiniteOfIsQuadraticExtension` `Module.Projective.of_free` `toFree` `le_iff_lt_or_eq` `minpoly.natDegree_le` `finrank_eq_two` `Polynomial.Splits.of_natDegree_le_one` `LE.le.trans` `Polynomial.natDegree_map_le` `Polynomial.Splits.of_natDegree_eq_two` `Polynomial.natDegree_map` `DivisionRing.isSimpleRing` `Polynomial.eval_map_algebraMap` `minpoly.aeval`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normal_iInf` 📖	mathematical	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`IsScalarTower.left` `iInf_le` `Algebra.IsAlgebraic.of_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Normal.toIsAlgebraic` `minpoly.algHom_eq` `Normal.splits'` `instIsDomain` `splits_iff_mem` `Polynomial.Splits.of_isScalarTower` `isScalarTower_mid'`
`normal_iSup` 📖	mathematical	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`IsScalarTower.left` `isAlgebraic_iSup` `Normal.toIsAlgebraic` `instIsDomain` `exists_finset_of_mem_supr''` `Normal.of_isSplittingField` `isSplittingField_iSup` `Finset.prod_ne_zero_iff` `Polynomial.nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `minpoly.ne_zero` `Normal.isIntegral` `adjoin_rootSet_isSplittingField` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `Polynomial.map_map` `Polynomial.Splits.map` `Normal.splits` `iSup_le` `le_iSup_of_le` `adjoin_le_iff` `Polynomial.Splits.image_rootSet` `DivisionRing.isSimpleRing` `minpoly_eq`
`normal_inf` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `normal_iInf` `iInf_bool_eq`
`normal_sup` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `normal_iSup` `iSup_bool_eq`
`splits_of_mem_adjoin` 📖	—	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin`	—	—	`instIsDomain` `IsScalarTower.left` `normal_iSup` `Normal.of_isSplittingField` `adjoin_rootSet_isSplittingField` `splits_of_splits` `le_iSup` `subset_adjoin` `nonempty_algHom_adjoin_of_splits` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `minpoly.algHom_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.map_map` `AlgHom.comp_algebraMap_of_tower` `isScalarTower` `Polynomial.Splits.map` `Normal.splits`

Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isSplittingField` 📖	mathematical	—	`Polynomial.IsSplittingField`	—	`isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.Splits.prod` `splits` `Polynomial.map_prod` `RelEmbedding.injective` `instIsDomain` `Algebra.top_toSubmodule` `eq_top_iff` `Module.Basis.span_eq` `Submodule.span_le` `Set.range_subset_iff` `Algebra.subset_adjoin` `Multiset.mem_toFinset` `Polynomial.mem_roots` `Polynomial.map_eq_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Finset.prod_ne_zero_iff` `Polynomial.nontrivial` `Polynomial.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `minpoly.ne_zero` `isIntegral` `Polynomial.IsRoot.def` `Polynomial.eval_map_algebraMap` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Finset.prod_eq_zero` `Finset.mem_univ` `minpoly.aeval`
`minpoly_eq_iff_mem_orbit` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Set` `Set.instMembership` `MulAction.orbit` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `DivisionSemiring.toGroupWithZero` `instSMulZeroClass` `AlgEquiv.aut` `MulSemiringAction.toMulDistribMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.applyMulSemiringAction`	—	`IntermediateField.exists_algHom_of_splits_of_aeval` `normal_iff` `minpoly.aeval` `AlgHom.normal_bijective` `IsScalarTower.right` `minpoly.algEquiv_eq`
`of_isSplittingField` 📖	mathematical	—	`Normal`	—	`eq_or_ne` `instIsDomain` `Polynomial.IsSplittingField.adjoin_rootSet` `of_algEquiv` `normal_self` `Algebra.bijective_algebraMap_iff` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.adjoin_empty` `Polynomial.rootSet_zero` `normal_iff` `IsIntegral.of_finite` `Polynomial.IsSplittingField.finiteDimensional` `Polynomial.SplittingField.splits` `Polynomial.splits_mul_iff` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `minpoly.ne_zero` `Polynomial.map_mul` `Polynomial.Splits.of_splits_map` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.map_map` `AlgHom.comp_algebraMap` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `Polynomial.IsSplittingField.map` `IntermediateField.isScalarTower_mid'` `IsScalarTower.algebraMap_eq` `IsScalarTower.of_algHom` `Polynomial.IsSplittingField.adjoin_rootSet_eq_range` `AlgHom.commutes` `IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen`

Polynomial.SplittingField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNormal` 📖	mathematical	—	`Normal` `Polynomial.SplittingField` `instField` `instAlgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.id`	—	`Normal.of_isSplittingField` `Polynomial.IsSplittingField.splittingField`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSolvable_of_isScalarTower` 📖	mathematical	—	`IsSolvable` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut`	—	`AlgHom.ext` `AlgEquiv.apply_symm_apply` `AlgEquiv.symm_apply_apply` `AlgEquiv.ext` `solvable_of_ker_le_range` `AlgEquiv.map_mul'` `AlgEquiv.map_add'` `AlgEquiv.restrictNormal_commutes` `AlgEquiv.ext_iff`

minpoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_algEquiv_of_root` 📖	mathematical	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `minpoly` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`AlgEquiv` `AlgEquiv.instFunLike`	—	`ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsAlgebraic.isIntegral` `IsScalarTower.left` `eq_of_root` `IntermediateField.isScalarTower_mid'` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `AlgEquiv.liftNormal_commutes` `algEquiv_apply` `IntermediateField.AdjoinSimple.algebraMap_gen`
`exists_algEquiv_of_root'` 📖	mathematical	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `minpoly` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`AlgEquiv` `AlgEquiv.instFunLike`	—	`exists_algEquiv_of_root` `AlgEquiv.symm_apply_apply`

---

← Back to Index