Integral

📁 Source: Mathlib/RingTheory/Algebraic/Integral.lean

Statistics

Metric	Count
Definitions `algebraicClosure`, `algEquivEquivAlgHom`	2
Theorems `bijective`, `exists_integral_multiples`, `finrank_of_isFractionRing`, `instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors`, `instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom`, `instIsPushout`, `instIsPushout_1`, `isAlgebraic_iff`, `isAlgebraic_iff_bot`, `isAlgebraic_iff_top`, `isBaseChange_of_isFractionRing`, `isIntegral`, `lift_rank_of_isFractionRing`, `of_finite`, `of_isIntegralClosure`, `rank_fractionRing`, `rank_fractionRing_mvPolynomial`, `rank_fractionRing_polynomial`, `rank_of_isFractionRing`, `tensorProduct`, `trans`, `trans_isIntegral`, `transcendental_iff`, `isAlgebraic`, `isAlgebraic_iff`, `isAlgebraic_iff_top`, `trans_isAlgebraic`, `transcendental_iff`, `isAlgebraic`, `isAlgebraic'`, `isAlgebraic_adjoin_iff`, `isAlgebraic_adjoin_of_nonempty`, `isAlgebraic_adjoin_singleton_iff`, `isAlgebraic_iff_isIntegral`, `add`, `adjoin_of_forall_isAlgebraic`, `exists_integral_multiple`, `iff_exists_smul_integral`, `isIntegral`, `mul`, `neg`, `nsmul`, `of_finite`, `of_mul`, `of_smul`, `of_smul_isIntegral`, `pow`, `restrictScalars`, `restrictScalars_of_isIntegral`, `smul`, `sub`, `tmul`, `zsmul`, `isAlgebraic`, `trans_isAlgebraic`, `exists_dvd_map_of_isAlgebraic`, `exists_dvd_map_of_isAlgebraic`, `algebraicClosure_eq_integralClosure`, `mem_algebraicClosure`, `extendScalars`, `extendScalars_of_isIntegral`, `integralClosure`, `subalgebraAlgebraicClosure`, `instFiniteDimensionalFractionRingOfFinite`, `instIsAlgebraicMvPolynomialOfNoZeroDivisors`, `instIsAlgebraicMvPolynomialOfNoZeroDivisors_1`, `instIsAlgebraicPolynomialOfNoZeroDivisors`, `instIsAlgebraicPolynomialOfNoZeroDivisors_1`, `instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure`, `instIsPushoutFractionRingMvPolynomial`, `instIsPushoutFractionRingMvPolynomial_1`, `instIsPushoutFractionRingPolynomial`, `instIsPushoutFractionRingPolynomial_1`, `integralClosure_le_algebraicClosure`, `isAlgebraic_iff_isIntegral`, `rank_mvPolynomial_mvPolynomial`, `rank_polynomial_polynomial`, `transcendental_aeval_iff`	78
Total	80

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `funLike`	—	`Algebra.IsAlgebraic.algHom_bijective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsAlgebraic.of_finite` `EuclideanDomain.toNontrivial`

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAlgebraic_adjoin_iff` 📖	mathematical	—	`Subalgebra.IsAlgebraic` `CommRing.toRing` `adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `IsAlgebraic`	—	`adjoin_le_iff`
`isAlgebraic_adjoin_of_nonempty` 📖	mathematical	`Set.Nonempty`	`Subalgebra.IsAlgebraic` `CommRing.toRing` `adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `IsAlgebraic`	—	`subset_adjoin` `isDomain_iff_noZeroDivisors_and_nontrivial` `IsAlgebraic.nontrivial` `isAlgebraic_adjoin_iff`
`isAlgebraic_adjoin_singleton_iff` 📖	mathematical	—	`Subalgebra.IsAlgebraic` `CommRing.toRing` `adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `IsAlgebraic`	—	`isAlgebraic_adjoin_of_nonempty` `Set.singleton_nonempty`
`isAlgebraic_iff_isIntegral` 📖	mathematical	—	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsIntegral`	—	`isAlgebraic_def` `isIntegral_def` `isAlgebraic_iff_isIntegral`

Algebra.IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_integral_multiples` 📖	mathematical	—	`IsIntegral` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`nontrivial` `Finset.prod_ne_zero_iff` `Finset.prod_erase_mul` `SemigroupAction.mul_smul` `IsIntegral.smul` `IsScalarTower.left` `IsAlgebraic.exists_integral_multiple` `isAlgebraic`
`finrank_of_isFractionRing` 📖	mathematical	—	`Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Cardinal.toNat_lift` `lift_rank_of_isFractionRing`
`instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors` 📖	mathematical	—	`IsLocalization` `CommRing.toCommSemiring` `Algebra.algebraMapSubmonoid` `CommSemiring.toSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero`	—	`Function.Injective.noZeroDivisors` `FaithfulSMul.algebraMap_injective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `IsLocalization.iff_of_le_of_exists_dvd` `map_le_nonZeroDivisors_of_injective` `le_rfl` `IsAlgebraic.exists_nonzero_dvd` `isAlgebraic` `mem_nonZeroDivisors_of_ne_zero`
`instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom` 📖	mathematical	—	`IsLocalizedModule` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `nonZeroDivisors` `Semiring.toMonoidWithZero` `AlgHom.toLinearMap` `IsScalarTower.toAlgHom`	—	`isLocalizedModule_iff_isLocalization` `instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors`
`instIsPushout` 📖	mathematical	—	`Algebra.IsPushout` `CommRing.toCommSemiring`	—	`Algebra.isPushout_iff` `isBaseChange_of_isFractionRing`
`instIsPushout_1` 📖	mathematical	—	`Algebra.IsPushout` `CommRing.toCommSemiring`	—	`Algebra.IsPushout.symm` `instIsPushout`
`isAlgebraic_iff` 📖	mathematical	—	`IsAlgebraic`	—	`IsAlgebraic.extendScalars` `FaithfulSMul.algebraMap_injective` `IsAlgebraic.restrictScalars`
`isAlgebraic_iff_bot` 📖	mathematical	—	`Algebra.IsAlgebraic` `CommRing.toRing`	—	`tower_bot_of_injective` `FaithfulSMul.algebraMap_injective` `trans`
`isAlgebraic_iff_top` 📖	mathematical	—	`Algebra.IsAlgebraic`	—	`isAlgebraic_iff`
`isBaseChange_of_isFractionRing` 📖	mathematical	—	`IsBaseChange` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.toModule` `AlgHom.toLinearMap` `IsScalarTower.toAlgHom`	—	`isLocalizedModule_iff_isBaseChange` `instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom`
`isIntegral` 📖	mathematical	—	`Algebra.IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Algebra.isAlgebraic_iff_isIntegral`
`lift_rank_of_isFractionRing` 📖	mathematical	—	`Cardinal.lift` `Module.rank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`IsLocalization.rank_eq` `le_rfl` `IsLocalizedModule.lift_rank_eq` `instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom`
`of_finite` 📖	mathematical	—	`Algebra.IsAlgebraic`	—	`Algebra.IsIntegral.isAlgebraic` `Algebra.IsIntegral.of_finite`
`of_isIntegralClosure` 📖	mathematical	—	`Algebra.IsAlgebraic` `CommRing.toRing`	—	`IsIntegralClosure.isIntegral_algebra` `Algebra.IsIntegral.isAlgebraic`
`rank_fractionRing` 📖	mathematical	—	`Module.rank` `FractionRing` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `Algebra.toModule` `OreLocalization.instCommSemiring` `FractionRing.liftAlgebra` `FractionRing.field` `OreLocalization.instAlgebra` `FractionRing.instFaithfulSMul`	—	`rank_of_isFractionRing` `Localization.isLocalization` `IsDomain.to_noZeroDivisors` `FractionRing.instFaithfulSMul` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left`
`rank_fractionRing_mvPolynomial` 📖	mathematical	—	`Module.rank` `FractionRing` `MvPolynomial` `CommRing.toCommSemiring` `MvPolynomial.instCommRingMvPolynomial` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `Algebra.toModule` `OreLocalization.instCommSemiring` `FractionRing.liftAlgebra` `FractionRing.field` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `OreLocalization.instAlgebra` `MvPolynomial.algebraMvPolynomial` `FractionRing.instFaithfulSMul` `MvPolynomial.instFaithfulSMul` `Cardinal.lift`	—	`IsDomain.of_faithfulSMul` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `FractionRing.instFaithfulSMul` `MvPolynomial.instFaithfulSMul` `rank_fractionRing` `instIsAlgebraicMvPolynomialOfNoZeroDivisors_1` `IsDomain.to_noZeroDivisors` `rank_mvPolynomial_mvPolynomial`
`rank_fractionRing_polynomial` 📖	mathematical	—	`Module.rank` `FractionRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `OreLocalization.instSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAddCommMonoidOreLocalization` `CommMonoid.toMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Semiring.toModule` `Algebra.toModule` `OreLocalization.instCommSemiring` `Polynomial.commSemiring` `FractionRing.liftAlgebra` `FractionRing.field` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `OreLocalization.instAlgebra` `Polynomial.algebra` `FractionRing.instFaithfulSMul` `instFaithfulSMulPolynomial`	—	`IsDomain.of_faithfulSMul` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `FractionRing.instFaithfulSMul` `instFaithfulSMulPolynomial` `rank_fractionRing` `instIsAlgebraicPolynomialOfNoZeroDivisors_1` `IsDomain.to_noZeroDivisors` `rank_polynomial_polynomial`
`rank_of_isFractionRing` 📖	mathematical	—	`Module.rank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Cardinal.lift_id` `lift_rank_of_isFractionRing`
`tensorProduct` 📖	mathematical	—	`Algebra.IsAlgebraic` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instRing` `CommRing.toRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `nontrivial` `Function.Injective.nontrivial` `FaithfulSMul.algebraMap_injective` `TensorProduct.induction_on` `isAlgebraic_zero` `IsAlgebraic.tmul` `isAlgebraic` `IsAlgebraic.add`
`trans` 📖	mathematical	—	`Algebra.IsAlgebraic`	—	`IsAlgebraic.restrictScalars` `isAlgebraic`
`trans_isIntegral` 📖	mathematical	—	`Algebra.IsAlgebraic`	—	`IsIntegral.trans_isAlgebraic` `Algebra.IsIntegral.isIntegral`
`transcendental_iff` 📖	mathematical	—	`Transcendental`	—	`Transcendental.extendScalars` `Transcendental.restrictScalars` `FaithfulSMul.algebraMap_injective`

Algebra.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic`	—	`IsIntegral.isAlgebraic` `isIntegral`
`isAlgebraic_iff` 📖	mathematical	—	`IsAlgebraic`	—	`IsAlgebraic.extendScalars` `FaithfulSMul.algebraMap_injective` `IsAlgebraic.restrictScalars_of_isIntegral`
`isAlgebraic_iff_top` 📖	mathematical	—	`Algebra.IsAlgebraic`	—	`isAlgebraic_iff`
`trans_isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic`	—	`IsAlgebraic.restrictScalars_of_isIntegral` `Algebra.IsAlgebraic.isAlgebraic`
`transcendental_iff` 📖	mathematical	—	`Transcendental`	—	`Transcendental.extendScalars_of_isIntegral` `Transcendental.restrictScalars` `FaithfulSMul.algebraMap_injective`

Algebra.IsPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `CommRing.toRing`	—	`symm` `AlgEquiv.isAlgebraic` `Algebra.to_smulCommClass` `Algebra.IsAlgebraic.tensorProduct`
`isAlgebraic'` 📖	mathematical	—	`Algebra.IsAlgebraic` `CommRing.toRing`	—	`AlgEquiv.isAlgebraic` `Algebra.to_smulCommClass` `Algebra.IsAlgebraic.tensorProduct`

IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsAlgebraic` `CommRing.toRing`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`exists_integral_multiple` `iff_exists_smul_integral` `isReduced_of_noZeroDivisors` `mul_ne_zero` `smul_add` `SemigroupAction.mul_smul` `mul_comm` `IsIntegral.add` `IsIntegral.smul` `IsScalarTower.left`
`adjoin_of_forall_isAlgebraic` 📖	—	`IsAlgebraic` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	—	—	`IsScalarTower.subalgebra'` `IsScalarTower.right` `Algebra.adjoin_le` `Algebra.subset_adjoin` `IsScalarTower.of_algebraMap_eq` `nontrivial` `Function.Injective.nontrivial` `Subtype.val_injective` `isDomain_iff_noZeroDivisors_and_nontrivial` `Subalgebra.noZeroDivisors` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `Subalgebra.isAlgebraic_iff` `Algebra.isAlgebraic_adjoin_iff` `isAlgebraic_algebraMap` `extendScalars` `Subalgebra.inclusion_injective` `restrictScalars` `IsScalarTower.subalgebra`
`exists_integral_multiple` 📖	mathematical	`IsAlgebraic`	`IsIntegral` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`Polynomial.leadingCoeff_eq_zero` `Polynomial.monic_integralNormalization` `Polynomial.integralNormalization_aeval_eq_zero` `map_eq_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Algebra.smul_def` `Mathlib.Tactic.Push.not_forall_eq` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `algebraMap_smul` `IsScalarTower.right` `MulZeroClass.zero_mul` `isIntegral_zero`
`iff_exists_smul_integral` 📖	mathematical	—	`IsAlgebraic` `IsIntegral` `Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`exists_integral_multiple` `of_smul_isIntegral` `isNilpotent_iff_eq_zero`
`isIntegral` 📖	mathematical	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IsIntegral`	—	`isAlgebraic_iff_isIntegral`
`mul` 📖	mathematical	`IsAlgebraic` `CommRing.toRing`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`exists_integral_multiple` `iff_exists_smul_integral` `isReduced_of_noZeroDivisors` `mul_ne_zero` `Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_mul_mul_comm` `IsIntegral.mul`
`neg` 📖	mathematical	`IsAlgebraic`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`EmbeddingLike.map_ne_zero_iff` `EquivLike.toEmbeddingLike` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Polynomial.aeval_comp` `Polynomial.aeval_neg` `Polynomial.aeval_X` `neg_neg`
`nsmul` 📖	mathematical	`IsAlgebraic`	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`smul` `Nat.cast_smul_eq_nsmul`
`of_finite` 📖	mathematical	—	`IsAlgebraic`	—	`IsIntegral.isAlgebraic` `IsIntegral.of_finite`
`of_mul` 📖	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `IsAlgebraic` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—	`exists_nonzero_eq_adjoin_mul` `mul` `Algebra.isAlgebraic_adjoin_singleton_iff` `of_smul` `mem_nonZeroDivisors_of_ne_zero` `Algebra.smul_def` `mul_right_comm`
`of_smul` 📖	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `IsAlgebraic` `Algebra.toSMul` `Ring.toSemiring`	—	—	`Polynomial.comp_C_mul_X_eq_zero_iff` `Polynomial.aeval_comp` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_C` `Polynomial.aeval_X` `Algebra.smul_def`
`of_smul_isIntegral` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsIntegral` `Algebra.toSMul` `Ring.toSemiring`	`IsAlgebraic`	—	`IsNilpotent.zero` `Polynomial.leadingCoeff_C_mul_X` `one_mul` `Polynomial.coeff_comp_degree_mul_degree` `Polynomial.natDegree_C_mul_X` `mul_one` `Polynomial.coeff_zero` `Polynomial.aeval_comp` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_C` `Polynomial.aeval_X` `Algebra.smul_def`
`pow` 📖	mathematical	`IsAlgebraic` `CommRing.toRing`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`nontrivial` `isAlgebraic_one` `pow_zero` `mul` `pow_succ`
`restrictScalars` 📖	—	`IsAlgebraic`	—	—	`NoZeroDivisors.of_faithfulSMul` `faithfulSMul_iff_algebraMap_injective` `Algebra.nontrivial_of_isAlgebraic` `NoZeroDivisors.to_isDomain` `Algebra.IsAlgebraic.exists_integral_multiples` `Polynomial.mem_coeffs_iff` `Finset.mem_image_of_mem` `Polynomial.support_smul` `Polynomial.map_ne_zero_iff` `Subtype.val_injective` `Polynomial.map_toSubring` `Polynomial.instIsTorsionFree` `FaithfulSMul.to_isTorsionFree` `NoZeroDivisors.to_isCancelMulZero` `IsDomain.toIsCancelMulZero` `Polynomial.eval_map_algebraMap` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Subalgebra.algebraMap_eq` `Polynomial.map_map` `Subalgebra.toSubring_subtype` `Polynomial.isScalarTower` `IsScalarTower.right` `AlgHom.restrictScalars_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `smul_zero` `restrictScalars_of_isIntegral` `IsScalarTower.subalgebra'` `Subalgebra.noZeroDivisors` `integralClosure.AlgebraIsIntegral` `Algebra.IsAlgebraic.isAlgebraic` `Algebra.isAlgebraic_of_not_injective` `Function.Injective.of_comp` `IsScalarTower.algebraMap_eq`
`restrictScalars_of_isIntegral` 📖	—	`IsAlgebraic`	—	—	`Function.Injective.noZeroDivisors` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `exists_integral_multiple` `subsingleton_or_nontrivial` `Module.subsingleton` `is_transcendental_of_subsingleton` `exists_nonzero_dvd` `IsIntegral.isAlgebraic` `Algebra.IsIntegral.isIntegral` `mem_nonZeroDivisors_of_ne_zero` `of_smul_isIntegral` `isNilpotent_iff_eq_zero` `isReduced_of_noZeroDivisors` `Algebra.smul_def` `IsScalarTower.algebraMap_apply` `mul_comm` `SemigroupAction.mul_smul` `isIntegral_trans` `IsIntegral.smul` `IsScalarTower.left` `Algebra.IsAlgebraic.isAlgebraic` `Algebra.isAlgebraic_of_not_injective` `Function.Injective.of_comp` `IsScalarTower.algebraMap_eq`
`smul` 📖	mathematical	`IsAlgebraic`	`Algebra.toSMul` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`Polynomial.scaleRoots_ne_zero` `Polynomial.scaleRoots_aeval_eq_zero` `Algebra.smul_def`
`sub` 📖	mathematical	`IsAlgebraic` `CommRing.toRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`add` `neg` `sub_eq_add_neg`
`tmul` 📖	mathematical	`IsAlgebraic`	`TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `CommSemiring.toSemiring` `Ring.toSemiring` `Algebra.TensorProduct.instRing` `CommRing.toRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `TensorProduct.tmul`	—	`Algebra.to_smulCommClass` `mul_one` `smul_eq_mul` `TensorProduct.smul_tmul'` `smul` `Polynomial.map_ne_zero_iff` `FaithfulSMul.algebraMap_injective` `Algebra.TensorProduct.includeRight_apply` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.coe_toRingHom` `Polynomial.map_aeval_eq_aeval_map` `RingHom.ext` `RingHomCompTriple.comp_apply` `RingHomCompTriple.right_ids` `AlgHom.comp_algebraMap_of_tower` `IsScalarTower.left` `TensorProduct.isScalarTower` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `IsScalarTower.right` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`zsmul` 📖	mathematical	`IsAlgebraic`	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`smul` `Int.cast_smul_eq_zsmul`

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAlgebraic` 📖	mathematical	`IsIntegral`	`IsAlgebraic`	—	`Polynomial.Monic.ne_zero`
`trans_isAlgebraic` 📖	mathematical	`IsIntegral`	`IsAlgebraic`	—	`subsingleton_or_nontrivial` `Algebra.IsAlgebraic.nontrivial` `isAlgebraic_zero` `Module.nontrivial` `IsAlgebraic.restrictScalars` `isAlgebraic`

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_dvd_map_of_isAlgebraic` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `instCommRingMvPolynomial` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `map` `algebraMap`	—	`IsAlgebraic.exists_nonzero_dvd` `Algebra.IsAlgebraic.isAlgebraic` `instIsAlgebraicMvPolynomialOfNoZeroDivisors_1` `mem_nonZeroDivisors_of_ne_zero` `instNoZeroDivisors`

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_dvd_map_of_isAlgebraic` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `map` `algebraMap`	—	`IsAlgebraic.exists_nonzero_dvd` `Algebra.IsAlgebraic.isAlgebraic` `instIsAlgebraicPolynomialOfNoZeroDivisors_1` `mem_nonZeroDivisors_of_ne_zero` `instNoZeroDivisors`

Subalgebra

Definitions

Name	Category	Theorems
`algebraicClosure` 📖	CompOp	7 math math: `mem_algebraicClosure`, `integralClosure_le_algebraicClosure`, `AlgebraicIndependent.subalgebraAlgebraicClosure`, `algebraicClosure_eq_integralClosure`, `Transcendental.subalgebraAlgebraicClosure`, `AlgebraicIndependent.matroid_closure_eq`, `instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicClosure_eq_integralClosure` 📖	mathematical	—	`algebraicClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `integralClosure`	—	`SetLike.ext` `instIsDomain` `isAlgebraic_iff_isIntegral`
`mem_algebraicClosure` 📖	mathematical	—	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `algebraicClosure` `IsAlgebraic` `CommRing.toRing`	—	—

Transcendental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extendScalars` 📖	—	`Transcendental`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `eq_1` `IsAlgebraic.restrictScalars`
`extendScalars_of_isIntegral` 📖	—	`Transcendental`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `eq_1` `IsAlgebraic.restrictScalars_of_isIntegral`
`integralClosure` 📖	mathematical	`Transcendental` `CommRing.toRing`	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	—	`extendScalars_of_isIntegral` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Subalgebra.noZeroDivisors` `integralClosure.AlgebraIsIntegral`
`subalgebraAlgebraicClosure` 📖	mathematical	`Transcendental` `CommRing.toRing`	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.algebraicClosure` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	—	`extendScalars` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Subalgebra.noZeroDivisors` `instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure`

(root)

Definitions

Name	Category	Theorems
`algEquivEquivAlgHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteDimensionalFractionRingOfFinite` 📖	mathematical	—	`FiniteDimensional` `FractionRing` `OreLocalization.instDivisionRingNonZeroDivisors` `CommRing.toRing` `IsDomain.toNontrivial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDomain.to_noZeroDivisors` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.instAddCommGroup` `CommMonoid.toMonoid` `Ring.toAddCommGroup` `Module.toDistribMulAction` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Algebra.toModule` `OreLocalization.instCommSemiring` `OreLocalization.instSemiring` `FractionRing.liftAlgebra` `FractionRing.field` `OreLocalization.instAlgebra` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero`	—	`IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `Module.Finite.exists_fin` `Module.finite_def` `Submodule.fg_span` `Set.toFinite` `Finite.Set.finite_image` `Finite.Set.finite_range` `Finite.of_fintype` `span_eq_top_localization_localization` `Localization.isLocalization` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `Algebra.IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors` `Algebra.IsAlgebraic.of_finite`
`instIsAlgebraicMvPolynomialOfNoZeroDivisors` 📖	mathematical	—	`Algebra.IsAlgebraic` `MvPolynomial` `CommRing.toCommSemiring` `MvPolynomial.instCommRingMvPolynomial` `CommRing.toRing` `MvPolynomial.algebraMvPolynomial`	—	`Algebra.IsPushout.isAlgebraic` `MvPolynomial.instNoZeroDivisors` `MvPolynomial.faithfulSMul` `instFaithfulSMul` `MvPolynomial.instIsScalarTower` `MvPolynomial.isScalarTower` `IsScalarTower.right` `MvPolynomial.instIsPushout`
`instIsAlgebraicMvPolynomialOfNoZeroDivisors_1` 📖	mathematical	—	`Algebra.IsAlgebraic` `MvPolynomial` `CommRing.toCommSemiring` `MvPolynomial.instCommRingMvPolynomial` `CommRing.toRing` `MvPolynomial.algebraMvPolynomial`	—	`Function.Injective.noZeroDivisors` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `instIsAlgebraicMvPolynomialOfNoZeroDivisors` `Algebra.isAlgebraic_of_not_injective` `MvPolynomial.map_injective_iff`
`instIsAlgebraicPolynomialOfNoZeroDivisors` 📖	mathematical	—	`Algebra.IsAlgebraic` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `Polynomial.ring` `CommRing.toRing` `Polynomial.algebra`	—	`Algebra.IsPushout.isAlgebraic` `Polynomial.instNoZeroDivisors` `Polynomial.faithfulSMul` `instFaithfulSMul` `instIsScalarTowerPolynomial` `IsScalarTower.left` `Polynomial.isScalarTower` `IsScalarTower.right` `instIsPushoutPolynomial`
`instIsAlgebraicPolynomialOfNoZeroDivisors_1` 📖	mathematical	—	`Algebra.IsAlgebraic` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `Polynomial.ring` `CommRing.toRing` `Polynomial.algebra`	—	`Function.Injective.noZeroDivisors` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `instIsAlgebraicPolynomialOfNoZeroDivisors` `Algebra.isAlgebraic_of_not_injective` `Polynomial.map_injective_iff`
`instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure` 📖	mathematical	—	`Algebra.IsAlgebraic` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.algebraicClosure` `Subalgebra.toRing` `CommRing.toRing` `Subalgebra.algebra`	—	`Subalgebra.isAlgebraic_iff`
`instIsPushoutFractionRingMvPolynomial` 📖	mathematical	—	`Algebra.IsPushout` `FractionRing` `MvPolynomial` `CommRing.toCommSemiring` `MvPolynomial.instCommRingMvPolynomial` `OreLocalization.instCommSemiring` `MvPolynomial.commSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAlgebra` `MvPolynomial.algebra` `Algebra.id` `FractionRing.liftAlgebra` `FractionRing.field` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.algebraMvPolynomial` `FractionRing.instFaithfulSMul` `MvPolynomial.instFaithfulSMul` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule` `IsScalarTower.right` `Algebra.toSMul` `MvPolynomial.isScalarTower` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `FractionRing.instIsScalarTower` `MvPolynomial.instIsScalarTower`	—	`MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `FractionRing.instFaithfulSMul` `MvPolynomial.instFaithfulSMul` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `MvPolynomial.isScalarTower` `FractionRing.instIsScalarTower` `MvPolynomial.instIsScalarTower` `IsScalarTower.left` `Algebra.IsPushout.comp_iff` `MvPolynomial.instIsPushout_1` `Algebra.IsAlgebraic.instIsPushout` `instIsAlgebraicMvPolynomialOfNoZeroDivisors_1` `IsDomain.to_noZeroDivisors` `MvPolynomial.instNoZeroDivisors` `Localization.isLocalization`
`instIsPushoutFractionRingMvPolynomial_1` 📖	mathematical	—	`Algebra.IsPushout` `CommRing.toCommSemiring` `FractionRing` `MvPolynomial` `MvPolynomial.instCommRingMvPolynomial` `OreLocalization.instCommSemiring` `MvPolynomial.commSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAlgebra` `MvPolynomial.algebra` `Algebra.id` `FractionRing.liftAlgebra` `FractionRing.field` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.algebraMvPolynomial` `FractionRing.instFaithfulSMul` `MvPolynomial.instFaithfulSMul` `FractionRing.instIsScalarTower` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule` `IsScalarTower.right` `Algebra.toSMul` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `MvPolynomial.instIsScalarTower` `MvPolynomial.isScalarTower` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul`	—	`Algebra.IsPushout.symm` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `FractionRing.instFaithfulSMul` `MvPolynomial.instFaithfulSMul` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `MvPolynomial.isScalarTower` `FractionRing.instIsScalarTower` `MvPolynomial.instIsScalarTower` `instIsPushoutFractionRingMvPolynomial`
`instIsPushoutFractionRingPolynomial` 📖	mathematical	—	`Algebra.IsPushout` `FractionRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `OreLocalization.instCommSemiring` `Polynomial.commSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `FractionRing.liftAlgebra` `FractionRing.field` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Polynomial.algebra` `FractionRing.instFaithfulSMul` `instFaithfulSMulPolynomial` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule` `IsScalarTower.right` `Algebra.toSMul` `Polynomial.isScalarTower` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `FractionRing.instIsScalarTower` `instIsScalarTowerPolynomial` `IsScalarTower.left` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `FractionRing.instFaithfulSMul` `instFaithfulSMulPolynomial` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Polynomial.isScalarTower` `FractionRing.instIsScalarTower` `instIsScalarTowerPolynomial` `IsScalarTower.left` `Algebra.IsPushout.comp_iff` `instIsPushoutPolynomial_1` `Algebra.IsAlgebraic.instIsPushout` `instIsAlgebraicPolynomialOfNoZeroDivisors_1` `IsDomain.to_noZeroDivisors` `Polynomial.instNoZeroDivisors` `Localization.isLocalization`
`instIsPushoutFractionRingPolynomial_1` 📖	mathematical	—	`Algebra.IsPushout` `CommRing.toCommSemiring` `FractionRing` `Polynomial` `CommSemiring.toSemiring` `Polynomial.commRing` `OreLocalization.instCommSemiring` `Polynomial.commSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAlgebra` `Polynomial.algebraOfAlgebra` `Algebra.id` `FractionRing.liftAlgebra` `FractionRing.field` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Polynomial.algebra` `FractionRing.instFaithfulSMul` `instFaithfulSMulPolynomial` `FractionRing.instIsScalarTower` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule` `IsScalarTower.right` `Algebra.toSMul` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `instIsScalarTowerPolynomial` `IsScalarTower.left` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.isScalarTower` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul`	—	`Algebra.IsPushout.symm` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `FractionRing.instFaithfulSMul` `instFaithfulSMulPolynomial` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Polynomial.isScalarTower` `FractionRing.instIsScalarTower` `instIsScalarTowerPolynomial` `IsScalarTower.left` `instIsPushoutFractionRingPolynomial`
`integralClosure_le_algebraicClosure` 📖	mathematical	—	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `integralClosure` `Subalgebra.algebraicClosure`	—	`IsIntegral.isAlgebraic` `IsDomain.toNontrivial`
`isAlgebraic_iff_isIntegral` 📖	mathematical	—	`IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsIntegral`	—	`Polynomial.monic_mul_leadingCoeff_inv` `Polynomial.aeval_def` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `MulZeroClass.zero_mul` `IsIntegral.isAlgebraic` `EuclideanDomain.toNontrivial`
`rank_mvPolynomial_mvPolynomial` 📖	mathematical	—	`Module.rank` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Algebra.toModule` `MvPolynomial.algebraMvPolynomial` `Cardinal.lift`	—	`IsBaseChange.lift_rank_eq` `MvPolynomial.instNoZeroDivisors` `MvPolynomial.faithfulSMul` `instFaithfulSMul` `MvPolynomial.instIsScalarTower` `MvPolynomial.isScalarTower` `IsScalarTower.right` `Algebra.isPushout_iff` `MvPolynomial.instIsPushout_1` `Cardinal.lift_umax` `Cardinal.lift_id'`
`rank_polynomial_polynomial` 📖	mathematical	—	`Module.rank` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `Algebra.toModule` `Polynomial.commSemiring` `Polynomial.algebra`	—	`IsBaseChange.rank_eq` `Polynomial.instNoZeroDivisors` `Polynomial.faithfulSMul` `instFaithfulSMul` `instIsScalarTowerPolynomial` `IsScalarTower.left` `Polynomial.isScalarTower` `IsScalarTower.right` `Algebra.isPushout_iff` `instIsPushoutPolynomial_1`
`transcendental_aeval_iff` 📖	mathematical	—	`Transcendental` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Ring.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.ring` `DivisionRing.toRing` `Field.toDivisionRing` `CommRing.toCommSemiring`	—	`Transcendental.eq_1` `Mathlib.Tactic.Contrapose.contrapose₄` `isAlgebraic_iff_isIntegral` `IsIntegral.of_mem_of_fg` `IsIntegral.fg_adjoin_singleton` `Polynomial.aeval_mem_adjoin_singleton` `Transcendental.of_aeval` `Transcendental.aeval_of_transcendental`

---

← Back to Index