Documentation Verification Report

SeparablyGenerated

📁 Source: Mathlib/FieldTheory/SeparablyGenerated.lean

Statistics

Metric	Count
Definitions `toPolynomialAdjoinImageCompl`	1
Theorems `aeval_toPolynomialAdjoinImageCompl_eq_zero`, `coeff_toPolynomialAdjoinImageCompl_ne_zero`, `exists_mem_support_not_dvd_of_forall_totalDegree_le`, `irreducible_of_forall_totalDegree_le`, `irreducible_toPolynomialAdjoinImageCompl`, `isAlgebraic_of_mem_vars_of_forall_totalDegree_le`, `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow`, `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'`, `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top`, `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType`, `exists_isTranscendenceBasis_and_isSeparable_of_perfectField`	11
Total	12

MvPolynomial

Definitions

Name	Category	Theorems
`toPolynomialAdjoinImageCompl` 📖	CompOp	2 math math: `aeval_toPolynomialAdjoinImageCompl_eq_zero`, `irreducible_toPolynomialAdjoinImageCompl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_toPolynomialAdjoinImageCompl_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Subalgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Polynomial` `Subalgebra.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Subalgebra.toAlgebra` `Polynomial.aeval` `toPolynomialAdjoinImageCompl`	—	`Polynomial.isScalarTower` `IsScalarTower.right` `IsScalarTower.subalgebra'` `AlgHom.restrictScalars_apply` `algHom_ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `rename_X` `aeval_X` `optionEquivLeft_X_some` `Polynomial.map_C` `Polynomial.aeval_C` `optionEquivLeft_X_none` `Polynomial.map_X` `Polynomial.aeval_X`
`coeff_toPolynomialAdjoinImageCompl_ne_zero` 📖	—	`totalDegree` `Semifield.toCommSemiring` `Field.toSemifield` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `support`	—	—	`AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Iff.not` `map_eq_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `rename_injective` `Subtype.val_injective` `optionEquivLeft_coeff_some_coeff_none` `notMem_support_iff` `coeff_zero` `renameEquiv_apply` `Equiv.optionSubtypeNe_none` `Equiv.symm_symm` `Finsupp.mapDomain_equiv_apply` `coeff_rename_mapDomain` `Equiv.injective` `Finsupp.equivMapDomain_eq_mapDomain` `map_zero` `Polynomial.coeff_map` `algHom_ext` `rename_X` `aeval_X` `totalDegree_coeff_optionEquivLeft_add_le` `totalDegree_renameEquiv` `LE.le.trans` `Finsupp.le_degree` `Nat.instCanonicallyOrderedAdd` `le_totalDegree` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `totalDegree_rename_le`
`exists_mem_support_not_dvd_of_forall_totalDegree_le` 📖	mathematical	`Nat.Prime` `LinearIndepOn` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `SetLike.coe` `Finset` `Finset.instSetLike` `totalDegree` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Finsupp` `Nat.instMulZeroClass` `Finset.instMembership` `support` `Finsupp.instFunLike`	—	`IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.ne_zero` `Finsupp.ext` `Mathlib.Tactic.Push.not_and_eq` `Finset.coe_image` `Finset.coe_univ` `Set.image_univ` `linearIndepOn_range_iff` `LinearIndependent.injective` `EuclideanDomain.toNontrivial` `LinearIndependent.linearIndepOn_id` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `monomial_pow` `one_pow` `Finset.sum_congr` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `LinearMap.semilinearMapClass` `mul_one` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `Finset.sum_attach` `support_sum_monomial_coeff` `SemilinearMapClass.distribMulActionSemiHomClass` `ne_of_ne_of_eq` `Finsupp.mapDomain_injective` `Finsupp.mapDomain_zero` `RingHomCompTriple.ids` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `Finsupp.mapDomain_single` `Finsupp.linearCombination_single` `one_smul` `totalDegree.eq_1` `Finset.mul_sup₀` `Finset.sup_le_iff` `Finset.mem_image` `Finsupp.mapDomain_support` `le_trans` `Finsupp.sum_smul_index` `Finsupp.mul_sum` `le_refl` `Finset.le_sup` `Mathlib.Tactic.Contrapose.contrapose₄` `totalDegree_eq_zero_iff_eq_C` `map_eq_zero` `RingHom.instRingHomClass` `aeval_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `LE.le.trans` `LE.le.trans_eq` `one_mul` `LT.lt.not_ge` `Nat.Prime.one_lt` `mul_le_mul_iff_of_pos_right` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Ne.bot_lt` `Function.sometimes_spec`
`irreducible_of_forall_totalDegree_le` 📖	mathematical	`totalDegree` `Semifield.toCommSemiring` `Field.toSemifield` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Irreducible` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsUnit.ne_zero` `EuclideanDomain.toNontrivial` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mul_ne_zero_iff` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `isUnit_iff_totalDegree_of_isReduced` `isReduced_of_noZeroDivisors` `nontrivial_of_nontrivial` `RingHom.instRingHomClass` `totalDegree_eq_zero_iff_eq_C` `nonpos_iff_eq_zero` `Nat.instCanonicallyOrderedAdd` `add_le_iff_nonpos_right` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `totalDegree_mul_of_isDomain` `mul_comm` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass`
`irreducible_toPolynomialAdjoinImageCompl` 📖	mathematical	`Irreducible` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `AlgebraicIndependent` `Set.Elem` `setOf` `Set` `Set.instMembership` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Polynomial` `Subalgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `Subalgebra.toSemiring` `Polynomial.semiring` `toPolynomialAdjoinImageCompl`	—	`Set.ext` `AlgEquiv.coe_algHom` `algHom_ext` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `aeval_X` `Irreducible.map` `RingEquivClass.toMulEquivClass` `AlgEquivClass.toRingEquivClass`
`isAlgebraic_of_mem_vars_of_forall_totalDegree_le` 📖	mathematical	`totalDegree` `Semifield.toCommSemiring` `Field.toSemifield` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset` `Finset.instMembership` `vars`	`IsAlgebraic` `Subalgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subalgebra.toCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Subalgebra.toAlgebra` `Ring.toSemiring`	—	`mem_vars` `coeff_toPolynomialAdjoinImageCompl_ne_zero` `Finsupp.mem_support_iff` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Polynomial.coeff_zero` `aeval_toPolynomialAdjoinImageCompl_eq_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow` 📖	mathematical	`Nat.Prime` `LinearIndepOn` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `SetLike.coe` `Finset` `Finset.instSetLike` `IsTranscendenceBasis`	`IsSeparable` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set.image` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `IntermediateField.toField` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id`	—	`Set.ext` `AlgebraicIndepOn.insert_iff` `Algebra.IsAlgebraic.isAlgebraic` `IsTranscendenceBasis.isAlgebraic` `EuclideanDomain.toNontrivial` `instWellFoundedLTNat` `Function.argminOn_mem` `Function.argminOn_le` `MvPolynomial.irreducible_of_forall_totalDegree_le` `MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le` `MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le` `MvPolynomial.mem_vars` `IsTranscendenceBasis.of_isAlgebraic_adjoin_image_compl` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `MvPolynomial.irreducible_toPolynomialAdjoinImageCompl` `MulEquiv.uniqueFactorizationMonoid` `MvPolynomial.uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `EuclideanDomain.to_principal_ideal_domain` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `MvPolynomial.coeff_toPolynomialAdjoinImageCompl_ne_zero` `Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map` `IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin` `Subalgebra.isDomain` `instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid` `Irreducible.isPrimitive` `Subalgebra.noZeroDivisors` `Polynomial.coeff_eq_zero_of_natDegree_lt` `Eq.trans_lt` `Mathlib.Tactic.Contrapose.contrapose₂` `expChar_of_injective_algebraMap` `IsScalarTower.left` `RingHom.injective` `DivisionRing.isSimpleRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Nat.Prime.ne_one` `Polynomial.separable_or` `minpoly.irreducible` `isAlgebraic_iff_isIntegral` `IntermediateField.isAlgebraic_adjoin_iff` `map_eq_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin` `Polynomial.coeff_map` `MulZeroClass.zero_mul` `eq_mul_inv_iff_mul_eq₀` `Irreducible.ne_zero` `Polynomial.coeff_expand` `Nat.Prime.pos` `Polynomial.coeff_mul_C` `minpoly.eq_of_irreducible` `Polynomial.aeval_map_algebraMap` `IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1` `MvPolynomial.aeval_toPolynomialAdjoinImageCompl_eq_zero`
`exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'` 📖	mathematical	`Nat.Prime` `LinearIndepOn` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `SetLike.coe` `Finset` `Finset.instSetLike` `IsTranscendenceBasis` `Set.Elem` `Set` `Set.instMembership`	`Set.instSDiff` `Set.instInsert` `Set.instSingletonSet` `IsSeparable` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set.image` `IntermediateField.toField` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id`	—	`exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow` `IsTranscendenceBasis.comp_equiv` `Set.ext` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass`
`exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top` 📖	mathematical	`Nat.Prime` `LinearIndepOn` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `SetLike.coe` `Finset` `Finset.instSetLike` `IntermediateField.adjoin` `Set.range` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsTranscendenceBasis`	`Algebra.IsSeparable` `SetLike.instMembership` `IntermediateField.instSetLike` `Set.image` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `IntermediateField.toField` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id`	—	`exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow` `separableClosure.eq_top_iff` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.restrictScalars_injective` `IntermediateField.restrictScalars_top` `eq_top_iff` `IntermediateField.adjoin_le_iff` `eq_or_ne` `isSeparable_algebraMap` `IntermediateField.subset_adjoin`
`exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType` 📖	mathematical	`Nat.Prime` `LinearIndepOn` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `SetLike.coe` `Finset` `Finset.instSetLike`	`IsTranscendenceBasis` `SetLike.instMembership` `Algebra.IsSeparable` `IntermediateField` `IntermediateField.instSetLike` `IntermediateField.adjoin` `IntermediateField.toField` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure` `of_not_not` `le_restrictScalars_separableClosure` `IntermediateField.subset_adjoin` `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'` `not_lt_iff_le_imp_ge` `SetLike.lt_iff_le_and_exists` `instIsConcreteLE` `separableClosure_le_separableClosure_iff` `IntermediateField.adjoin_le_iff` `eq_or_ne` `Set.image_id`
`exists_isTranscendenceBasis_and_isSeparable_of_perfectField` 📖	mathematical	—	`IsTranscendenceBasis` `Finset` `SetLike.instMembership` `Finset.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.IsSeparable` `IntermediateField` `IntermediateField.instSetLike` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.toField` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield`	—	`CharP.exists'` `IsDomain.to_noZeroDivisors` `instIsDomain` `EuclideanDomain.toNontrivial` `IntermediateField.fg_top` `IntermediateField.isAlgebraic_adjoin_iff_top` `Algebra.isAlgebraic_iff_isIntegral` `Algebra.isIntegral_of_surjective` `AlgEquiv.surjective` `IsScalarTower.left` `exists_isTranscendenceBasis_subset` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `Set.Finite.subset` `Finset.finite_toSet` `Subtype.range_coe_subtype` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsTranscendenceBasis.isAlgebraic_field` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `PerfectField.ofCharZero` `IntermediateField.charZero` `Fact.out` `CharP.of_ringHom_of_ne_zero` `Nat.Prime.ne_zero` `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType` `LinearIndependent.map_of_injective_injective` `PerfectField.toPerfectRing` `expChar_prime` `EquivLike.toEmbeddingLike` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `isReduced_of_noZeroDivisors` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `add_pow_expChar` `Algebra.smul_def` `mul_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `frobeniusEquiv_symm_pow`

---

← Back to Index