Documentation Verification Report

Extension

📁 Source: Mathlib/FieldTheory/Extension.lean

Statistics

Metric	Count
Definitions `IsExtendible`, `carrier`, `emb`, `instInhabited`, `instOrderBot`, `instPartialOrder`, `union`	7
Theorems `range_eval_eq_rootSet_minpoly_of_splits`, `carrier_union`, `eq_iff`, `eq_iff_le_carrier_eq`, `exists_lift_of_splits`, `exists_lift_of_splits'`, `exists_upper_bound`, `le_iff`, `le_of_carrier_le_iSup`, `le_union`, `lt_iff`, `lt_iff_le_carrier_ne`, `nonempty_algHom_of_exist_lifts_finset`, `union_isExtendible`, `exists_algHom_adjoin_of_splits`, `exists_algHom_adjoin_of_splits'`, `exists_algHom_adjoin_of_splits_of_aeval`, `exists_algHom_of_adjoin_splits`, `exists_algHom_of_adjoin_splits'`, `exists_algHom_of_adjoin_splits_of_aeval`, `exists_algHom_of_splits`, `exists_algHom_of_splits'`, `exists_algHom_of_splits_of_aeval`, `nonempty_algHom_adjoin_of_splits`, `nonempty_algHom_of_adjoin_splits`, `nonempty_algHom_of_splits`	26
Total	33

Algebra.IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_eval_eq_rootSet_minpoly_of_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Set.range` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DFunLike.coe` `AlgHom.funLike` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain`	—	`Set.ext` `instIsDomain` `Polynomial.mem_rootSet_of_ne` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsIntegral.isIntegral` `isIntegral` `Polynomial.aeval_algHom_apply` `AlgHom.algHomClass` `minpoly.aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `IntermediateField.exists_algHom_of_splits_of_aeval`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_algHom_adjoin_of_splits` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `adjoin`	`AlgHom` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `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` `AlgHom.comp` `Field.toCommRing` `inclusion`	—	`IsScalarTower.left` `zorn_le_nonempty_Ici₀` `Lifts.exists_upper_bound` `le_rfl` `adjoin_le_iff` `Lifts.exists_lift_of_splits` `AlgHom.ext`
`exists_algHom_adjoin_of_splits'` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `AlgHom.toRingHom` `Semifield.toCommSemiring` `minpoly`	`AlgHom` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `algebra'` `Algebra.toSMul` `AlgHom.restrictDomain` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SubfieldClass.toSubringClass` `Field.toDivisionRing` `instSubfieldClass` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `isScalarTower`	—	`IsScalarTower.left` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isScalarTower_mid'` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `instIsScalarTowerSubtypeMem_1` `IsScalarTower.right` `IsScalarTower.of_algebraMap_eq'` `IsIntegral.tower_top` `IsIntegral.minpoly_splits_tower_top'` `RingHom.ext` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.symm_apply_apply` `isScalarTower` `instIsConcreteLE` `subset_adjoin_of_subset_left` `le_rfl` `subset_adjoin` `AlgHom.ext`
`exists_algHom_adjoin_of_splits_of_aeval` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`AlgHom` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `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` `DFunLike.coe` `AlgHom.funLike`	—	`IsScalarTower.left` `isAlgebraic_adjoin` `Algebra.IsAlgebraic.isAlgebraic` `adjoin_simple_le_iff` `instIsDomain` `isIntegral_iff` `isAlgebraic_iff_isIntegral` `Polynomial.mem_aroots` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `exists_algHom_adjoin_of_splits` `DFunLike.congr_fun` `algHomAdjoinIntegralEquiv_symm_apply_gen`
`exists_algHom_of_adjoin_splits` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly` `adjoin` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.comp` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `val`	—	`IsScalarTower.left` `le_top` `exists_algHom_adjoin_of_splits`
`exists_algHom_of_adjoin_splits'` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `AlgHom.toRingHom` `Semifield.toCommSemiring` `minpoly` `adjoin` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.restrictDomain`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsScalarTower.left` `isScalarTower` `exists_algHom_adjoin_of_splits'`
`exists_algHom_of_adjoin_splits_of_aeval` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly` `adjoin` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DFunLike.coe` `AlgHom.funLike`	—	`IsScalarTower.left` `mem_top` `exists_algHom_adjoin_of_splits_of_aeval`
`exists_algHom_of_splits` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.comp` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `val`	—	`IsScalarTower.left` `exists_algHom_of_adjoin_splits` `adjoin_univ`
`exists_algHom_of_splits'` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `AlgHom.toRingHom` `Semifield.toCommSemiring` `minpoly`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.restrictDomain`	—	`exists_algHom_of_adjoin_splits'` `adjoin_univ`
`exists_algHom_of_splits_of_aeval` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DFunLike.coe` `AlgHom.funLike`	—	`exists_algHom_of_adjoin_splits_of_aeval` `adjoin_univ`
`nonempty_algHom_adjoin_of_splits` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly`	`AlgHom` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `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` `bot_le` `exists_algHom_adjoin_of_splits`
`nonempty_algHom_of_adjoin_splits` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly` `adjoin` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IsScalarTower.left` `exists_algHom_of_adjoin_splits`
`nonempty_algHom_of_splits` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`nonempty_algHom_of_adjoin_splits` `adjoin_univ`

IntermediateField.Lifts

Definitions

Name	Category	Theorems
`IsExtendible` 📖	MathDef	1 math math: `union_isExtendible`
`carrier` 📖	CompOp	7 math math: `exists_lift_of_splits'`, `eq_iff_le_carrier_eq`, `lt_iff`, `exists_lift_of_splits`, `eq_iff`, `carrier_union`, `le_iff`
`emb` 📖	CompOp	3 math math: `lt_iff`, `eq_iff`, `le_iff`
`instInhabited` 📖	CompOp	—
`instOrderBot` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	9 math math: `lt_iff_le_carrier_ne`, `exists_lift_of_splits'`, `eq_iff_le_carrier_eq`, `le_union`, `lt_iff`, `exists_lift_of_splits`, `le_of_carrier_le_iSup`, `exists_upper_bound`, `le_iff`
`union` 📖	CompOp	3 math math: `le_union`, `union_isExtendible`, `carrier_union`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carrier_union` 📖	mathematical	`IsChain` `IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`carrier` `union` `iSup` `IntermediateField` `Set.Elem` `IntermediateField.Lifts` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Set` `Set.instMembership`	—	`le_antisymm` `iSup_le` `bot_le` `le_iSup_of_le` `le_rfl`
`eq_iff` 📖	mathematical	—	`IntermediateField` `carrier` `AlgHom.comp` `SetLike.instMembership` `IntermediateField.instSetLike` `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` `Field.toCommRing` `Module.toDistribMulAction` `Algebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `emb` `IntermediateField.inclusion` `Eq.le` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder`	—	`IsScalarTower.left` `Eq.le` `eq_iff_le_carrier_eq` `le_iff`
`eq_iff_le_carrier_eq` 📖	mathematical	—	`IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `carrier`	—	`Eq.le` `LE.le.antisymm` `Eq.ge`
`exists_lift_of_splits` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `algebraMap` `Semifield.toCommSemiring` `minpoly`	`IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `carrier`	—	`exists_lift_of_splits'` `IsIntegral.tower_top` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IsIntegral.minpoly_splits_tower_top'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap`
`exists_lift_of_splits'` 📖	mathematical	`IsIntegral` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `carrier` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.map` `AlgHom.toRingHom` `IntermediateField.algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `emb` `minpoly`	`IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `carrier`	—	`IsScalarTower.left` `LT.lt.ne'` `minpoly.degree_pos` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.isScalarTower_mid'` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `instIsDomain` `Polynomial.degree_map` `DivisionRing.isSimpleRing` `Polynomial.mem_aroots` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `minpoly.ne_zero` `SubsemiringClass.nontrivial` `Polynomial.eval_map` `Polynomial.eval_rootOfSplits` `IsScalarTower.of_algebraMap_eq` `IntermediateField.algebraMap_mem` `AlgHom.commutes` `IntermediateField.mem_adjoin_simple_self`
`exists_upper_bound` 📖	mathematical	`IsChain` `IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`le_union`
`le_iff` 📖	mathematical	—	`IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IntermediateField` `IntermediateField.instPartialOrder` `carrier` `AlgHom.comp` `SetLike.instMembership` `IntermediateField.instSetLike` `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` `Field.toCommRing` `Module.toDistribMulAction` `Algebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `emb` `IntermediateField.inclusion`	—	`IsScalarTower.left`
`le_of_carrier_le_iSup` 📖	mathematical	`IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IntermediateField` `IntermediateField.instPartialOrder` `carrier` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice`	`IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`IsScalarTower.left` `le_iff` `LE.le.trans` `iSup_le` `IntermediateField.algHom_ext_of_eq_adjoin` `LE.le.antisymm` `IntermediateField.iSup_eq_adjoin` `Eq.ge` `IntermediateField.subset_adjoin` `Set.mem_iUnion`
`le_union` 📖	mathematical	`IsChain` `IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set` `Set.instMembership`	`IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `union`	—	`Set.mem_insert_of_mem` `le_iSup` `Subalgebra.iSupLift_inclusion` `Set.instNonemptyElemInsert`
`lt_iff` 📖	mathematical	—	`IntermediateField.Lifts` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `IntermediateField` `IntermediateField.instPartialOrder` `carrier` `AlgHom.comp` `SetLike.instMembership` `IntermediateField.instSetLike` `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` `Field.toCommRing` `Module.toDistribMulAction` `Algebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `emb` `IntermediateField.inclusion` `LT.lt.le`	—	`IsScalarTower.left` `LT.lt.le` `lt_iff_le_carrier_ne` `le_iff` `LE.le.lt_of_ne` `LT.lt.ne`
`lt_iff_le_carrier_ne` 📖	mathematical	—	`IntermediateField.Lifts` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Preorder.toLE`	—	`lt_iff_le_and_ne`
`nonempty_algHom_of_exist_lifts_finset` 📖	mathematical	`IntermediateField.Lifts` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `IntermediateField` `IntermediateField.instSetLike` `carrier`	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`bot_le` `zorn_le₀` `isEmpty_or_nonempty` `union_isExtendible` `le_union` `SetLike.exists_of_lt` `instIsConcreteLE` `Ne.lt_top` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `IntermediateField.finiteDimensional_adjoin` `Finite.of_fintype` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsAlgebraic.tower_top` `IntermediateField.isScalarTower_mid'` `IntermediateField.instIsScalarTowerSubtypeMem_1` `IsScalarTower.right` `IsScalarTower.of_algHom` `LT.lt.le` `lt_iff` `IntermediateField.restrictScalars_adjoin_eq_sup` `AlgHom.coe_ringHom_injective` `AlgHom.comp_algebraMap` `maximal_iff_forall_gt` `instIsDomain` `sup_le_iff` `IntermediateField.adjoin_simple_le_iff` `Set.iUnion_true` `Set.iUnion_congr_Prop` `Finset.coe_univ` `Finset.coe_biUnion` `Finset.coe_singleton` `Finset.coe_union` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Push.not_and_eq` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`union_isExtendible` 📖	mathematical	`IsChain` `IntermediateField.Lifts` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsExtendible`	`IsExtendible` `union`	—	`IsScalarTower.left` `IntermediateField.finiteDimensional_adjoin` `Finite.of_fintype` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `Directed.finite_le` `instIsTransLe` `Finite.algHom` `Module.Free.of_divisionRing` `instIsDomain` `IsChain.directed` `instReflLe` `IntermediateField.adjoin_le_iff` `LE.le.trans` `sup_le` `le_sup_left` `le_sup_right` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Push.not_and_eq` `le_iff` `IntermediateField.isScalarTower_mid'` `IntermediateField.restrictScalars_adjoin` `IntermediateField.adjoin.mono` `Set.union_subset_union_left` `IntermediateField.algHom_ext_of_eq_adjoin` `Eq.ge` `IntermediateField.subset_adjoin` `IsChain.total` `le_of_carrier_le_iSup` `le_union` `Eq.le` `carrier_union` `iSup_range'` `HasSubset.Subset.trans` `Set.instIsTransSubset` `SetLike.coe_subset_coe` `instIsConcreteLE` `le_iSup_of_le` `le_rfl`

---

← Back to Index