Documentation Verification Report

PrimitiveElement

📁 Source: Mathlib/FieldTheory/PrimitiveElement.lean

Statistics

Metric	Count
Definitions `powerBasisOfFiniteOfSeparable`	1
Theorems `card`, `card_of_splits`, `natCard_of_splits`, `of_exists_primitive_element`, `of_finite_intermediateField`, `exists_primitive_element`, `exists_primitive_element_iff_finite_intermediateField`, `exists_primitive_element_of_finite_bot`, `exists_primitive_element_of_finite_intermediateField`, `exists_primitive_element_of_finite_top`, `finite_intermediateField_of_exists_primitive_element`, `isAlgebraic_of_adjoin_eq_adjoin`, `isAlgebraic_of_finite_intermediateField`, `primitive_element_iff_algHom_eq_of_eval`, `primitive_element_iff_algHom_eq_of_eval'`, `primitive_element_iff_minpoly_degree_eq`, `primitive_element_iff_minpoly_natDegree_eq`, `primitive_element_inf_aux`, `primitive_element_inf_aux_exists_c`	19
Total	20

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card` 📖	mathematical	—	`Fintype.card` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `minpoly.AlgHom.fintype` `DivisionRing.toRing` `Field.toDivisionRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`card_of_splits` `IsAlgClosed.splits`
`card_of_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Fintype.card` `AlgHom` `minpoly.AlgHom.fintype` `instIsDomain` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`instIsDomain` `Fintype.card_eq_nat_card` `natCard_of_splits`
`natCard_of_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Nat.card` `AlgHom` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`natCard_of_powerBasis` `Algebra.IsSeparable.isSeparable` `PowerBasis.finrank` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`

Field

Definitions

Name	Category	Theorems
`powerBasisOfFiniteOfSeparable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_primitive_element` 📖	mathematical	—	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`isEmpty_or_nonempty` `IntermediateField.adjoin_zero` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.adjoin_simple_adjoin_simple` `primitive_element_inf_aux` `isEmpty_fintype` `IntermediateField.induction_on_adjoin` `exists_primitive_element_of_finite_bot` `Finite.of_fintype`
`exists_primitive_element_iff_finite_intermediateField` 📖	mathematical	—	`Algebra.IsAlgebraic` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Finite`	—	`finite_intermediateField_of_exists_primitive_element` `isAlgebraic_of_finite_intermediateField` `exists_primitive_element_of_finite_intermediateField`
`exists_primitive_element_of_finite_bot` 📖	mathematical	—	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`exists_primitive_element_of_finite_top` `Module.finite_of_finite`
`exists_primitive_element_of_finite_intermediateField` 📖	mathematical	—	`IntermediateField.adjoin` `Set` `Set.instSingletonSet`	—	`finite_or_infinite` `IsScalarTower.left` `exists_primitive_element_of_finite_bot` `IntermediateField.finiteDimensional_left` `FiniteDimensional.of_finite_intermediateField` `IntermediateField.lift_adjoin_simple` `IntermediateField.lift_top` `IntermediateField.induction_on_adjoin` `IntermediateField.adjoin_zero` `IntermediateField.isScalarTower_mid'` `IntermediateField.adjoin_simple_adjoin_simple`
`exists_primitive_element_of_finite_top` 📖	mathematical	—	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`IsCyclic.exists_generator` `instIsCyclicUnitsOfFinite` `instIsDomain` `instFiniteUnits` `eq_top_iff` `IntermediateField.zero_mem` `Set.mem_range` `Units.val_mk0` `zpow_mem` `SubfieldClass.toSubgroupClass` `IntermediateField.instSubfieldClass` `IntermediateField.mem_adjoin_simple_self`
`finite_intermediateField_of_exists_primitive_element` 📖	mathematical	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Finite`	—	`Finite.of_fintype` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `instIsLocalRing` `minpoly.ne_zero_of_finite` `FiniteDimensional.of_exists_primitive_element` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Polynomial.Monic.map` `minpoly.monic` `IsIntegral.of_finite` `IntermediateField.finiteDimensional_right` `IsScalarTower.left` `Polynomial.map_map` `Polynomial.map_dvd` `minpoly.dvd_map_of_isScalarTower` `IntermediateField.isScalarTower_mid'` `IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element` `Finite.of_injective`
`isAlgebraic_of_adjoin_eq_adjoin` 📖	mathematical	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield`	`IsAlgebraic` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	—	`IntermediateField.mem_bot` `IntermediateField.mem_adjoin_simple_self` `pow_zero` `IntermediateField.adjoin_one` `Polynomial.X_pow_sub_C_ne_zero` `IsLocalRing.toNontrivial` `instIsLocalRing` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Polynomial.aeval_X` `Polynomial.aeval_C` `sub_self` `IntermediateField.mem_adjoin_simple_iff` `isAlgebraic_zero` `div_zero` `pow_eq_zero_iff` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `sub_eq_zero` `eq_div_iff` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Int.instCharZero` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Nat.cast_zero` `Polynomial.coeff_sub` `Polynomial.coeff_X_pow_mul` `Polynomial.coeff_expand_mul'` `Polynomial.coeff_expand` `sub_zero` `Polynomial.leadingCoeff_ne_zero` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Polynomial.expand_aeval` `Ne.lt_or_gt`
`isAlgebraic_of_finite_intermediateField` 📖	mathematical	—	`Algebra.IsAlgebraic` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	—	`Finite.exists_ne_map_eq_of_infinite` `instInfiniteNat` `isAlgebraic_of_adjoin_eq_adjoin`
`primitive_element_iff_algHom_eq_of_eval` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`primitive_element_iff_algHom_eq_of_eval'` `IntermediateField.eq_of_le_of_finrank_eq'` `IntermediateField.finiteDimensional_right` `le_top` `IntermediateField.finrank_top` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `instIsDomain` `AlgHom.card_of_splits` `IntermediateField.isSeparable_tower_top` `IsIntegral.minpoly_splits_tower_top` `IntermediateField.isScalarTower_mid'` `IsScalarTower.of_algHom` `IsIntegral.of_finite` `Fintype.card_eq_one_iff` `AlgHom.restrictScalars_injective` `AlgHom.commutes`
`primitive_element_iff_algHom_eq_of_eval'` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `toEuclideanDomain` `DivisionRing.toRing` `toDivisionRing`	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `AlgHom` `DFunLike.coe` `AlgHom.funLike`	—	`instIsDomain` `Polynomial.card_rootSet_eq_natDegree` `Algebra.IsSeparable.isSeparable` `Set.toFinset_congr` `Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `instIsLocalRing` `AlgHom.card_of_splits` `Set.toFinset_range` `Finset.coe_univ`
`primitive_element_iff_minpoly_degree_eq` 📖	mathematical	—	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `toEuclideanDomain` `minpoly` `DivisionRing.toRing` `toDivisionRing` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring`	—	`Polynomial.degree_eq_iff_natDegree_eq` `minpoly.ne_zero_of_finite` `primitive_element_iff_minpoly_natDegree_eq`
`primitive_element_iff_minpoly_natDegree_eq` 📖	mathematical	—	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `toEuclideanDomain` `minpoly` `DivisionRing.toRing` `toDivisionRing` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring`	—	`IsScalarTower.left` `IntermediateField.adjoin.finrank` `IsIntegral.of_finite` `finrank_top` `IntermediateField.eq_of_le_of_finrank_eq` `IntermediateField.finiteDimensional_left` `le_top`
`primitive_element_inf_aux` 📖	mathematical	—	`IntermediateField.adjoin` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`Algebra.IsSeparable.isIntegral` `instIsDomain` `primitive_element_inf_aux_exists_c` `IsScalarTower.left` `IntermediateField.adjoin.algebraMap_mem` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `instIsLocalRing` `minpoly.ne_zero` `EuclideanDomain.gcd_eq_zero_iff` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Polynomial.separable_gcd_right` `Polynomial.Separable.map` `Algebra.IsSeparable.isSeparable` `Polynomial.eval_gcd_eq_zero` `Polynomial.eval_comp` `Polynomial.eval_sub` `Polynomial.eval_mul` `Polynomial.eval_C` `Polynomial.eval_X` `Polynomial.eval_map_algebraMap` `Algebra.smul_def` `add_sub_cancel_right` `minpoly.aeval` `Polynomial.gcd_map` `Polynomial.Splits.of_dvd` `Polynomial.SplittingField.splits` `EuclideanDomain.gcd_dvd_right` `Polynomial.root_left_of_root_gcd` `Polynomial.mem_roots_map` `Polynomial.eval₂_map` `Polynomial.eval₂_X` `Polynomial.eval₂_C` `Polynomial.eval₂_mul` `Polynomial.eval₂_sub` `Polynomial.eval₂_comp` `Polynomial.root_right_of_root_gcd` `div_eq_iff` `sub_ne_zero` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.add_pf_add_gt` `Polynomial.eq_X_sub_C_of_separable_of_root_eq` `Polynomial.map_comp` `Polynomial.map_map` `IntermediateField.isScalarTower_mid'` `Polynomial.map_sub` `Polynomial.map_C` `Polynomial.map_mul` `Polynomial.map_X` `SubfieldClass.toSubgroupClass` `SubringClass.toNegMemClass` `map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `map_neg` `mul_sub` `Polynomial.coeff_sub` `Polynomial.mul_coeff_zero` `Polynomial.coeff_C` `Polynomial.coeff_X_zero` `MulZeroClass.mul_zero` `zero_sub` `neg_neg` `Polynomial.coeff_mul_X` `Polynomial.coeff_mul_C` `Polynomial.coeff_C_succ` `MulZeroClass.zero_mul` `sub_zero` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `Polynomial.leadingCoeff_eq_zero` `Subtype.mem` `le_antisymm` `IntermediateField.adjoin_le_iff` `IntermediateField.sub_mem` `IntermediateField.mem_adjoin_simple_self` `Subalgebra.smul_mem` `IntermediateField.adjoin_simple_le_iff` `IntermediateField.subset_adjoin` `Set.mem_insert` `Set.mem_insert_of_mem` `IntermediateField.add_mem` `IntermediateField.smul_mem`
`primitive_element_inf_aux_exists_c` 📖	—	—	—	—	`instIsDomain` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `instIsLocalRing` `Infinite.exists_notMem_finset` `Mathlib.Tactic.Push.not_and_eq`

Field.FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_exists_primitive_element` 📖	mathematical	`IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`FiniteDimensional` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Algebra.toModule` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IsScalarTower.left` `IntermediateField.adjoin.finiteDimensional` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `LinearEquiv.finiteDimensional`
`of_finite_intermediateField` 📖	mathematical	—	`FiniteDimensional` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Algebra.toModule` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.isAlgebraic_of_finite_intermediateField` `IsScalarTower.left` `IntermediateField.finiteDimensional_iSup_of_finite` `Subtype.finite` `IntermediateField.adjoin.finiteDimensional` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `LE.le.antisymm` `le_top` `le_iSup` `IntermediateField.mem_adjoin_simple_self` `LinearEquiv.finiteDimensional`

---

← Back to Index