Basic

📁 Source: Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Statistics

Metric	Count
Definitions `gen₁`, `gen₂`, `powerBasis`, `adjoinRootEquivAdjoin`, `algHomAdjoinIntegralEquiv`, `fintypeOfAlgHomAdjoinIntegral`, `powerBasisAux`, `equivAdjoinSimple`, `algEquiv`	9
Theorems `algebraMap_gen₁`, `algebraMap_gen₂`, `of_restrictScalars`, `finiteDimensional`, `finrank`, `powerBasis_dim`, `powerBasis_gen`, `adjoinRootEquivAdjoin_apply_root`, `adjoinRootEquivAdjoin_symm_apply_gen`, `adjoin_eq_top_of_adjoin_eq_top`, `adjoin_finite_isCompactElement`, `adjoin_finset_isCompactElement`, `adjoin_minpoly_coeff_of_exists_primitive_element`, `adjoin_rank_le_of_isAlgebraic`, `adjoin_rank_le_of_isAlgebraic_left`, `adjoin_rank_le_of_isAlgebraic_right`, `adjoin_root_eq_top`, `adjoin_simple_isCompactElement`, `aeval_gen_minpoly`, `algHomAdjoinIntegralEquiv_symm_apply_gen`, `bot_eq_top_iff_finrank_eq_one`, `bot_eq_top_of_finrank_adjoin_eq_one`, `bot_eq_top_of_finrank_adjoin_le_one`, `bot_eq_top_of_rank_adjoin_eq_one`, `card_algHom_adjoin_integral`, `cardinalMk_adjoin_le`, `coe_iSup_of_directed`, `exists_finset_of_mem_adjoin`, `exists_finset_of_mem_iSup`, `exists_finset_of_mem_supr'`, `exists_finset_of_mem_supr''`, `exists_lt_finrank_of_infinite_dimensional`, `finiteDimensional_adjoin`, `finiteDimensional_adjoin_pair`, `finiteDimensional_iSup_of_finite`, `finiteDimensional_iSup_of_finset`, `finiteDimensional_iSup_of_finset'`, `finiteDimensional_sup`, `finrank_adjoin_eq_one_iff`, `finrank_adjoin_simple_eq_one_iff`, `finrank_bot`, `finrank_bot'`, `finrank_eq_one_iff`, `finrank_eq_one_iff_eq_top`, `finrank_sup_le`, `finrank_top`, `finrank_top'`, `forall_mem_adjoin_smul_eq_self_iff`, `instFiniteSubtypeMemBot`, `instIsCompactlyGenerated`, `isAlgebraic_adjoin`, `isAlgebraic_adjoin_pair`, `isAlgebraic_adjoin_simple`, `isAlgebraic_iSup`, `isSimpleOrder_of_finrank_prime`, `isSplittingField_iSup`, `lift_cardinalMk_adjoin_le`, `mem_adjoin_iff`, `mem_adjoin_pair_left`, `mem_adjoin_pair_right`, `mem_adjoin_range_iff`, `mem_adjoin_simple_iff`, `minpoly_gen`, `rank_adjoin_eq_one_iff`, `rank_adjoin_simple_eq_one_iff`, `rank_bot`, `rank_bot'`, `rank_eq_one_iff`, `rank_sup_le_of_isAlgebraic`, `rank_top`, `rank_top'`, `restrictScalars_le_iff`, `subsingleton_of_finrank_adjoin_eq_one`, `subsingleton_of_finrank_adjoin_le_one`, `subsingleton_of_rank_adjoin_eq_one`, `toSubalgebra_iSup_of_directed`, `irreducible_comp`, `equivAdjoinSimple_aeval`, `equivAdjoinSimple_gen`, `equivAdjoinSimple_symm_aeval`, `equivAdjoinSimple_symm_gen`, `algEquiv_apply`, `degree_dvd`, `degree_le`, `eq_of_root`, `natDegree_le`	86
Total	95

IntermediateField

Definitions

Name	Category	Theorems
`adjoinRootEquivAdjoin` 📖	CompOp	2 math math: `adjoinRootEquivAdjoin_symm_apply_gen`, `adjoinRootEquivAdjoin_apply_root`
`algHomAdjoinIntegralEquiv` 📖	CompOp	1 math math: `algHomAdjoinIntegralEquiv_symm_apply_gen`
`fintypeOfAlgHomAdjoinIntegral` 📖	CompOp	—
`powerBasisAux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoinRootEquivAdjoin_apply_root` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `AlgEquiv` `AdjoinRoot` `minpoly` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AdjoinRoot.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `AdjoinRoot.instAlgebra` `Algebra.id` `algebra'` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgEquiv.instFunLike` `adjoinRootEquivAdjoin` `AdjoinRoot.root` `AdjoinSimple.gen`	—	`AdjoinRoot.lift_root` `IsScalarTower.left` `aeval_gen_minpoly`
`adjoinRootEquivAdjoin_symm_apply_gen` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `AlgEquiv` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `AdjoinRoot` `minpoly` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AdjoinRoot.instCommRing` `algebra'` `Algebra.toSMul` `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` `AdjoinRoot.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `adjoinRootEquivAdjoin` `AdjoinSimple.gen` `AdjoinRoot.root`	—	`IsScalarTower.left` `AlgEquiv.symm_apply_eq` `adjoinRootEquivAdjoin_apply_root`
`adjoin_eq_top_of_adjoin_eq_top` 📖	—	`adjoin` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—	`restrictScalars_injective` `restrictScalars_top` `top_le_iff` `adjoin_le_iff` `coe_restrictScalars` `le_refl`
`adjoin_finite_isCompactElement` 📖	mathematical	—	`IsCompactElement` `IntermediateField` `instPartialOrder` `adjoin`	—	`adjoin_finset_isCompactElement` `Set.Finite.coe_toFinset`
`adjoin_finset_isCompactElement` 📖	mathematical	—	`IsCompactElement` `IntermediateField` `instPartialOrder` `adjoin` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`biSup_adjoin_simple` `iSup_congr_Prop` `CompleteLattice.isCompactElement_finsetSup` `adjoin_simple_isCompactElement`
`adjoin_minpoly_coeff_of_exists_primitive_element` 📖	mathematical	`adjoin` `Set` `Set.instSingletonSet` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`SetLike.coe` `Finset` `Finset.instSetLike` `Polynomial.coeffs` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `SetLike.instMembership` `instSetLike` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `instSubfieldClass` `algebraMap` `instAlgebraSubtypeMem` `Algebra.id` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `Ring.toSemiring`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `adjoin_le_iff` `Finset.mem_coe` `Polynomial.mem_coeffs_iff` `Polynomial.coeff_map` `Subtype.mem` `subset_adjoin` `minpoly.dvd` `Polynomial.aeval_def` `Polynomial.eval₂_eq_eval_map` `Polynomial.map_toSubring` `Polynomial.eval_map_algebraMap` `minpoly.aeval` `IsScalarTower.left` `adjoin.finrank` `IsIntegral.of_finite` `finiteDimensional_right` `finrank_top'` `adjoin_eq_top_of_adjoin_eq_top` `isScalarTower_mid'` `eq_of_le_of_finrank_le'` `Polynomial.natDegree_toSubring` `Polynomial.natDegree_map` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.natDegree_le_of_dvd` `SubsemiringClass.noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.Monic.ne_zero` `Subring.instNontrivialSubtypeMem` `Polynomial.monic_toSubring` `Polynomial.Monic.map` `minpoly.monic`
`adjoin_rank_le_of_isAlgebraic` 📖	mathematical	`Algebra.IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`Cardinal` `Cardinal.instLE` `Module.rank` `adjoin` `SetLike.coe` `module'`	—	`IsScalarTower.left` `adjoin_intermediateField_toSubalgebra_of_isAlgebraic` `Subalgebra.adjoin_rank_le` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `LinearEquiv.rank_eq`
`adjoin_rank_le_of_isAlgebraic_left` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `SetLike.coe` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`adjoin_rank_le_of_isAlgebraic` `IsScalarTower.left`
`adjoin_rank_le_of_isAlgebraic_right` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `SetLike.coe` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.left` `adjoin_rank_le_of_isAlgebraic`
`adjoin_root_eq_top` 📖	mathematical	—	`adjoin` `AdjoinRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AdjoinRoot.instField` `AdjoinRoot.instAlgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.id` `Set` `Set.instSingletonSet` `AdjoinRoot.root` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`eq_adjoin_of_eq_algebra_adjoin` `AdjoinRoot.adjoinRoot_eq_top`
`adjoin_simple_isCompactElement` 📖	mathematical	—	`IsCompactElement` `IntermediateField` `instPartialOrder` `adjoin` `Set` `Set.instSingletonSet`	—	`sSup_eq_iSup'` `Set.Nonempty.to_subtype` `Set.mem_iUnion` `coe_iSup_of_directed` `DirectedOn.directed_val` `SetLike.mem_coe`
`aeval_gen_minpoly` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `Polynomial.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `Polynomial.algebraOfAlgebra` `Algebra.id` `algebra'` `Algebra.toSMul` `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.funLike` `Polynomial.aeval` `AdjoinSimple.gen` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SubsemiringClass.toAddSubmonoidClass` `Semiring.toNonAssocSemiring` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass`	—	`IsScalarTower.left` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `AdjoinSimple.algebraMap_gen` `Polynomial.aeval_algebraMap_apply` `isScalarTower_mid'` `minpoly.aeval`
`algHomAdjoinIntegralEquiv_symm_apply_gen` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`DFunLike.coe` `AlgHom` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `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` `Module.toDistribMulAction` `Algebra.toModule` `AlgHom.funLike` `Equiv` `Multiset` `Multiset.instMembership` `Polynomial.aroots` `minpoly` `instIsDomain` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `algHomAdjoinIntegralEquiv` `AdjoinSimple.gen`	—	`instIsDomain` `PowerBasis.lift_gen` `IsScalarTower.left` `adjoin.powerBasis_gen` `minpoly_gen` `Polynomial.mem_aroots` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`bot_eq_top_iff_finrank_eq_one` 📖	mathematical	—	`Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop` `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`	—	`finrank_bot'` `finrank_eq_one_iff_eq_top`
`bot_eq_top_of_finrank_adjoin_eq_one` 📖	mathematical	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	`IsScalarTower.left` `ext` `mem_top` `finrank_adjoin_simple_eq_one_iff`
`bot_eq_top_of_finrank_adjoin_le_one` 📖	mathematical	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	`IsScalarTower.left` `bot_eq_top_of_finrank_adjoin_eq_one` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_one` `Nat.cast_zero` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `finiteDimensional_left` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add`
`bot_eq_top_of_rank_adjoin_eq_one` 📖	mathematical	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Cardinal` `Cardinal.instOne`	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	`IsScalarTower.left` `ext` `mem_top` `rank_adjoin_simple_eq_one_iff`
`card_algHom_adjoin_integral` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IsSeparable` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly`	`Nat.card` `AlgHom` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `toField` `algebra'` `Algebra.toSMul` `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` `Polynomial.natDegree` `CommRing.toCommSemiring`	—	`IsScalarTower.left` `Nat.card_eq_fintype_card` `instIsDomain` `AlgHom.card_of_powerBasis` `minpoly_gen`
`cardinalMk_adjoin_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Set.Elem` `Cardinal.aleph0`	—	`Cardinal.lift_id` `lift_cardinalMk_adjoin_le`
`coe_iSup_of_directed` 📖	mathematical	`Directed` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iUnion`	—	`Subalgebra.coe_iSup_of_directed` `Set.mem_iUnion` `inv_mem` `le_antisymm` `iSup_le` `le_iSup` `Set.iUnion_subset`
`exists_finset_of_mem_adjoin` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin`	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`exists_finset_of_mem_iSup` `biSup_adjoin_simple` `Finset.coe_image` `Subtype.coe_preimage_self` `SetLike.le_def` `instIsConcreteLE` `subset_adjoin`
`exists_finset_of_mem_iSup` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `instSetLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	`Finset` `Finset.instMembership`	—	`CompleteLattice.IsCompactElement.exists_finset_of_le_iSup` `adjoin_simple_isCompactElement`
`exists_finset_of_mem_supr'` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `instSetLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	`Finset` `Finset.instMembership` `adjoin` `Set` `Set.instSingletonSet`	—	`exists_finset_of_mem_iSup` `SetLike.le_def` `instIsConcreteLE` `iSup_le` `le_iSup_of_le` `mem_adjoin_simple_self`
`exists_finset_of_mem_supr''` 📖	mathematical	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	`Finset` `Finset.instMembership` `adjoin` `Polynomial.rootSet` `minpoly` `instIsDomain`	—	`IsScalarTower.left` `exists_finset_of_mem_iSup` `instIsDomain` `SetLike.le_def` `instIsConcreteLE` `iSup_le` `le_iSup_of_le` `minpoly_eq` `le_refl` `subset_adjoin` `Polynomial.mem_rootSet_of_ne` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isIntegral_iff` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `minpoly.aeval`
`exists_lt_finrank_of_infinite_dimensional` 📖	mathematical	`FiniteDimensional` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Algebra.toModule` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `module'` `DivisionRing.toDivisionSemiring` `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` `Module.finrank`	—	`IsScalarTower.left` `Subalgebra.finite_bot` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instFiniteSubtypeMemBot` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `Mathlib.Tactic.Contrapose.contrapose₂` `LinearEquiv.finiteDimensional` `eq_top_iff` `finiteDimensional_sup` `adjoin.finiteDimensional` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `by_contra` `eq_of_le_of_finrank_le` `le_sup_left` `LE.le.trans` `not_lt` `le_sup_right` `mem_adjoin_simple_self`
`finiteDimensional_adjoin` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Ring.toAddCommGroup` `toField` `module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction`	—	`IsScalarTower.left` `biSup_adjoin_simple` `iSup_subtype''` `finiteDimensional_iSup_of_finite` `adjoin.finiteDimensional`
`finiteDimensional_adjoin_pair` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instInsert` `Set.instSingletonSet` `Ring.toAddCommGroup` `toField` `module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction`	—	`IsScalarTower.left` `adjoin.finiteDimensional` `Set.singleton_union` `adjoin_union` `finiteDimensional_sup`
`finiteDimensional_iSup_of_finite` 📖	mathematical	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `instSetLike` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `toField` `module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `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`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`IsScalarTower.left` `iSup_univ` `Set.Finite.induction_on` `Set.finite_univ` `iSup_emptyset` `LinearEquiv.finiteDimensional` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `iSup_insert` `finiteDimensional_sup`
`finiteDimensional_iSup_of_finset` 📖	mathematical	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `instSetLike` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `toField` `module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `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`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Finset` `Finset.instMembership`	—	`IsScalarTower.left` `finiteDimensional_iSup_of_finite` `Finite.of_fintype` `iSup_subtype''`
`finiteDimensional_iSup_of_finset'` 📖	mathematical	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `instSetLike` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `toField` `module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `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`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Finset` `Finset.instMembership`	—	`IsScalarTower.left` `Subtype.forall'` `finiteDimensional_iSup_of_finite` `Finite.of_fintype` `iSup_subtype''`
`finiteDimensional_sup` 📖	mathematical	—	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `toField` `module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `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` `Algebra.TensorProduct.productMap_range` `range_val` `sup_toSubalgebra_of_left` `LinearMap.finiteDimensional_range` `Module.Finite.tensorProduct`
`finrank_adjoin_eq_one_iff` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Set` `Set.instHasSubset` `SetLike.coe` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `finrank_eq_one_iff` `adjoin_eq_bot_iff`
`finrank_adjoin_simple_eq_one_iff` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `finrank_adjoin_eq_one_iff` `Set.singleton_subset_iff`
`finrank_bot` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.left` `finrank_eq_one_iff`
`finrank_bot'` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem` `Semiring.toModule` `Algebra.toModule` `Semifield.toCommSemiring`	—	`rank_bot'`
`finrank_eq_one_iff` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `finrank_eq_finrank_subalgebra` `Subalgebra.finrank_eq_one_iff` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `bot_toSubalgebra`
`finrank_eq_one_iff_eq_top` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem` `Semiring.toModule` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Subalgebra.bot_eq_top_iff_finrank_eq_one` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `top_le_iff` `mem_top` `finrank_top`
`finrank_sup_le` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.left` `Subalgebra.finrank_sup_le_of_free` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `sup_toSubalgebra_of_left` `LinearMap.rank_le_of_injective` `Submodule.inclusion_injective` `Cardinal.toNat_apply_of_aleph0_le` `not_lt` `Module.rank_lt_aleph0_iff` `FiniteDimensional.eq_1` `LE.le.trans` `MulZeroClass.zero_mul` `le_refl`
`finrank_top` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem` `Semiring.toModule`	—	`Module.rank_eq_one_iff_finrank_eq_one` `rank_top`
`finrank_top'` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`finrank_top`
`forall_mem_adjoin_smul_eq_self_iff` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `Ring.toSemiring`	—	`instIsConcreteLE` `adjoin_le_iff`
`instFiniteSubtypeMemBot` 📖	mathematical	—	`Module.Finite` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`Subalgebra.finite_bot`
`instIsCompactlyGenerated` 📖	mathematical	—	`IsCompactlyGenerated` `IntermediateField` `instCompleteLattice`	—	`adjoin_simple_isCompactElement` `sSup_image` `biSup_adjoin_simple` `le_antisymm` `adjoin_le_iff` `le_rfl` `subset_adjoin`
`isAlgebraic_adjoin` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `biSup_adjoin_simple` `iSup_subtype''` `isAlgebraic_iSup` `isAlgebraic_adjoin_simple`
`isAlgebraic_adjoin_pair` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instInsert` `Set.instSingletonSet` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	—	`isAlgebraic_adjoin`
`isAlgebraic_adjoin_simple` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `adjoin.finiteDimensional` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`isAlgebraic_iSup` 📖	mathematical	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`IsScalarTower.left` `exists_finset_of_mem_supr'` `isAlgebraic_iff` `IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `finiteDimensional_iSup_of_finset` `adjoin.finiteDimensional` `isIntegral_iff` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral`
`isSimpleOrder_of_finrank_prime` 📖	mathematical	`Nat.Prime` `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`	`IsSimpleOrder` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	—	`Nat.prime_one_false` `bot_eq_top_iff_finrank_eq_one` `StrictMono.apply_eq_bot_iff` `toSubalgebra_strictMono` `StrictMono.apply_eq_top_iff` `IsSimpleOrder.eq_bot_or_eq_top` `Subalgebra.isSimpleOrder_of_finrank_prime` `instIsDomain`
`isSplittingField_iSup` 📖	mathematical	`Polynomial.IsSplittingField` `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` `Finset` `Finset.instMembership` `Finset.prod` `Polynomial` `CommRing.toCommMonoid` `Polynomial.commRing`	—	`IsScalarTower.left` `le_iSup_of_le` `le_iSup` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `instIsDomain` `Polynomial.map_prod` `Polynomial.Splits.prod` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.map_map` `AlgHom.comp_algebraMap_of_tower` `isScalarTower` `Polynomial.Splits.map` `Polynomial.rootSet_prod` `GaloisConnection.l_iSup₂` `gc` `iSup_congr`
`lift_cardinalMk_adjoin_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Set.Elem` `Cardinal.aleph0`	—	`adjoin_toSubfield` `LE.le.trans` `Cardinal.lift_le` `Subfield.cardinalMk_closure_le_max` `Cardinal.lift_max` `sup_le_iff` `Cardinal.lift_aleph0` `Cardinal.mk_union_le` `Cardinal.add_le_max` `le_imp_le_of_le_of_le` `sup_le_sup` `Cardinal.mk_range_le_lift` `le_refl` `le_sup_right`
`mem_adjoin_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `DFunLike.coe` `AlgHom` `MvPolynomial` `Set` `Set.instMembership` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval`	—	`mem_adjoin_range_iff` `Subtype.range_coe`
`mem_adjoin_pair_left` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`subset_adjoin` `Set.mem_insert`
`mem_adjoin_pair_right` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`subset_adjoin` `Set.mem_insert_of_mem` `Set.mem_singleton`
`mem_adjoin_range_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set.range` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `DFunLike.coe` `AlgHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval`	—	`Algebra.adjoin_range_eq_range_aeval`
`mem_adjoin_simple_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `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`	—	`Algebra.adjoin_singleton_eq_range_aeval`
`minpoly_gen` 📖	mathematical	—	`minpoly` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule` `AdjoinSimple.gen`	—	`IsScalarTower.left` `minpoly.algebraMap_eq` `isScalarTower_mid'` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `AdjoinSimple.algebraMap_gen`
`rank_adjoin_eq_one_iff` 📖	mathematical	—	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Cardinal` `Cardinal.instOne` `Set` `Set.instHasSubset` `SetLike.coe` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `rank_eq_one_iff` `adjoin_eq_bot_iff`
`rank_adjoin_simple_eq_one_iff` 📖	mathematical	—	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Cardinal` `Cardinal.instOne` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `rank_adjoin_eq_one_iff` `Set.singleton_subset_iff`
`rank_bot` 📖	mathematical	—	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Cardinal` `Cardinal.instOne`	—	`IsScalarTower.left` `rank_eq_one_iff`
`rank_bot'` 📖	mathematical	—	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem` `Semiring.toModule` `Algebra.toModule` `Semifield.toCommSemiring`	—	`IsScalarTower.left` `rank_mul_rank` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `Module.Free.of_divisionRing` `isScalarTower_mid'` `rank_bot` `one_mul`
`rank_eq_one_iff` 📖	mathematical	—	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Cardinal` `Cardinal.instOne` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `rank_eq_rank_subalgebra` `Subalgebra.rank_eq_one_iff` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `bot_toSubalgebra`
`rank_sup_le_of_isAlgebraic` 📖	mathematical	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule`	`Cardinal` `Cardinal.instLE` `Module.rank` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `module'` `Cardinal.instMul`	—	`IsScalarTower.left` `Subalgebra.rank_sup_le_of_free` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `sup_toSubalgebra_of_isAlgebraic`
`rank_top` 📖	mathematical	—	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem` `Semiring.toModule` `Cardinal` `Cardinal.instOne`	—	`Subalgebra.bot_eq_top_iff_rank_eq_one` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `top_le_iff`
`rank_top'` 📖	mathematical	—	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`rank_top`
`restrictScalars_le_iff` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `restrictScalars`	—	—
`subsingleton_of_finrank_adjoin_eq_one` 📖	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	—	`IsScalarTower.left` `subsingleton_of_bot_eq_top` `bot_eq_top_of_finrank_adjoin_eq_one`
`subsingleton_of_finrank_adjoin_le_one` 📖	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	—	`IsScalarTower.left` `subsingleton_of_bot_eq_top` `bot_eq_top_of_finrank_adjoin_le_one`
`subsingleton_of_rank_adjoin_eq_one` 📖	—	`Module.rank` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Cardinal` `Cardinal.instOne`	—	—	`IsScalarTower.left` `subsingleton_of_bot_eq_top` `bot_eq_top_of_rank_adjoin_eq_one`
`toSubalgebra_iSup_of_directed` 📖	mathematical	`Directed` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`toSubalgebra` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.instCompleteLatticeSubalgebra`	—	`isEmpty_or_nonempty` `iSup_of_empty` `SetLike.ext'` `coe_iSup_of_directed` `Subalgebra.coe_iSup_of_directed`

IntermediateField.AdjoinPair

Definitions

Name	Category	Theorems
`gen₁` 📖	CompOp	1 math math: `algebraMap_gen₁`
`gen₂` 📖	CompOp	1 math math: `algebraMap_gen₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_gen₁` 📖	mathematical	—	`DFunLike.coe` `RingHom` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instInsert` `Set.instSingletonSet` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `IntermediateField.instAlgebraSubtypeMem` `Algebra.id` `gen₁`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass`
`algebraMap_gen₂` 📖	mathematical	—	`DFunLike.coe` `RingHom` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instInsert` `Set.instSingletonSet` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `IntermediateField.instAlgebraSubtypeMem` `Algebra.id` `gen₂`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass`

IntermediateField.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_restrictScalars` 📖	—	`IntermediateField.FG` `IntermediateField.restrictScalars`	—	—	`le_antisymm` `IntermediateField.adjoin_le_iff` `LE.le.trans_eq` `IntermediateField.subset_adjoin` `IntermediateField.restrictScalars_le_iff`

IntermediateField.adjoin

Definitions

Name	Category	Theorems
`powerBasis` 📖	CompOp	2 math math: `powerBasis_gen`, `powerBasis_dim`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteDimensional` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `Ring.toAddCommGroup` `IntermediateField.toField` `IntermediateField.module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction`	—	`PowerBasis.finite` `IsScalarTower.left`
`finrank` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Module.finrank` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IntermediateField.toField` `IntermediateField.module'` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Polynomial.natDegree` `CommRing.toCommSemiring` `minpoly`	—	`IsScalarTower.left` `PowerBasis.finrank` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`powerBasis_dim` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`PowerBasis.dim` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule` `powerBasis` `Polynomial.natDegree` `minpoly`	—	`IsScalarTower.left`
`powerBasis_gen` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`PowerBasis.gen` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Module.toDistribMulAction` `Algebra.toModule` `powerBasis` `IntermediateField.AdjoinSimple.gen`	—	`IsScalarTower.left`

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_comp` 📖	mathematical	`Monic` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `IntermediateField.toField` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `IntermediateField.algebra'` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `IntermediateField.AdjoinSimple.gen`	`comp`	—	`IsScalarTower.left` `not_irreducible_C` `eq_C_of_natDegree_eq_zero` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `AdjoinRoot.instIsScalarTower` `IsScalarTower.right` `RingHom.map_sub` `coeff_map` `map_C` `AdjoinRoot.minpoly_root` `Irreducible.ne_zero` `inv_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `natDegree_comp` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `natDegree_eq_zero_of_isUnit` `WfDvdMonoid.exists_irreducible_factor` `UniqueFactorizationMonoid.toIsWellFounded` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `minpoly.eq_of_irreducible_of_monic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `aeval_comp` `aeval_eq_zero_of_dvd_aeval_eq_zero` `AdjoinRoot.eval₂_root` `IntermediateField.adjoin.finrank` `IsIntegral.of_finite` `PowerBasis.finite` `IntermediateField.mem_adjoin_simple_self` `AdjoinRoot.aeval_eq` `aeval_sub` `aeval_map_algebraMap` `IntermediateField.isScalarTower_mid'` `aeval_C` `sub_self` `Monic.sub_of_left` `Monic.map` `degree_lt_degree` `natDegree_C` `natDegree_map` `DivisionRing.isSimpleRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `IntermediateField.restrictScalars_injective` `IntermediateField.restrictScalars_top` `IntermediateField.adjoin_adjoin_left` `Set.union_comm` `IntermediateField.adjoin_root_eq_top` `IntermediateField.restrictScalars_adjoin` `Set.union_singleton` `Set.insert_eq_of_mem` `IntermediateField.adjoin_univ` `IntermediateField.finrank_top'` `IntermediateField.finiteDimensional_right` `natDegree_sub_C` `Module.finrank_mul_finrank` `commRing_strongRankCondition` `Module.Free.of_divisionRing` `AdjoinRoot.powerBasis_dim` `PowerBasis.finrank` `Associated.irreducible` `associated_of_dvd_of_natDegree_le` `Eq.ge`

PowerBasis

Definitions

Name	Category	Theorems
`equivAdjoinSimple` 📖	CompOp	4 math math: `equivAdjoinSimple_symm_aeval`, `equivAdjoinSimple_aeval`, `equivAdjoinSimple_gen`, `equivAdjoinSimple_symm_gen`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivAdjoinSimple_aeval` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `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` `Module.toDistribMulAction` `Algebra.toModule` `AlgEquiv.instFunLike` `equivAdjoinSimple` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.aeval` `IntermediateField.AdjoinSimple.gen`	—	`equivOfMinpoly_aeval`
`equivAdjoinSimple_gen` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `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` `Module.toDistribMulAction` `Algebra.toModule` `AlgEquiv.instFunLike` `equivAdjoinSimple` `IntermediateField.AdjoinSimple.gen`	—	`equivOfMinpoly_gen`
`equivAdjoinSimple_symm_aeval` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `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` `Module.toDistribMulAction` `Algebra.toModule` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equivAdjoinSimple` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.aeval` `IntermediateField.AdjoinSimple.gen`	—	`IsScalarTower.left` `equivAdjoinSimple.eq_1` `equivOfMinpoly_symm` `equivOfMinpoly_aeval` `IntermediateField.adjoin.powerBasis_gen`
`equivAdjoinSimple_symm_gen` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `gen` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `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` `Module.toDistribMulAction` `Algebra.toModule` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equivAdjoinSimple` `IntermediateField.AdjoinSimple.gen`	—	`IsScalarTower.left` `equivAdjoinSimple.eq_1` `equivOfMinpoly_symm` `equivOfMinpoly_gen` `IntermediateField.adjoin.powerBasis_gen`

minpoly

Definitions

Name	Category	Theorems
`algEquiv` 📖	CompOp	1 math math: `algEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquiv_apply` 📖	mathematical	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `minpoly`	`DFunLike.coe` `AlgEquiv` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `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` `Module.toDistribMulAction` `Algebra.toModule` `AlgEquiv.instFunLike` `algEquiv` `IntermediateField.AdjoinSimple.gen`	—	`ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsAlgebraic.isIntegral` `aeval` `IsScalarTower.left` `algEquiv.eq_1` `AlgEquiv.trans_apply` `IntermediateField.adjoinRootEquivAdjoin_apply_root` `AlgEquiv.symm_apply_apply` `AdjoinRoot.algEquivOfEq_root`
`degree_dvd` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpoly` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring`	—	`dvd_iff_exists_eq_mul_left` `IsScalarTower.left` `IntermediateField.adjoin.finrank` `mul_comm` `Module.finrank_mul_finrank` `IntermediateField.isScalarTower_mid'` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Module.Free.of_divisionRing`
`degree_le` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring`	—	`Polynomial.degree_le_of_natDegree_le` `natDegree_le`
`eq_of_root` 📖	—	`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`	—	—	`eq_iff_aeval_minpoly_eq_zero` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsAlgebraic.isIntegral`
`natDegree_le` 📖	mathematical	—	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring`	—	`IsScalarTower.left` `IntermediateField.adjoin.finrank` `IsIntegral.of_finite` `Submodule.finrank_le` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`

---

← Back to Index