Documentation Verification Report

ZariskisMainTheorem

📁 Source: Mathlib/RingTheory/ZariskisMainTheorem.lean

Statistics

Metric	Count
Definitions `ZariskisMainProperty`	1
Theorems `exists_fg_and_exists_notMem_and_awayMap_bijective`, `of_isOpen_singleton_fiber`, `of_quasiFiniteAt_residueField`, `of_weaklyQuasiFiniteAt`, `exists_fg_and_exists_notMem_and_awayMap_bijective`, `of_finiteType`, `of_finiteType_of_weaklyQuasiFiniteAt`, `of_isIntegral`, `quasiFiniteAt`, `restrictScalars`, `trans`, `not_isStronglyTranscendental_of_quasiFiniteAt`, `not_isStronglyTranscendental_of_weaklyQuasiFiniteAt`, `quasiFiniteAt_iff_isOpen_singleton_fiber`, `zariskisMainProperty_iff`, `zariskisMainProperty_iff'`, `zariskisMainProperty_iff_exists_saturation_eq_top`, `exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range`, `exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range`, `exists_leadingCoeff_pow_smul_mem_conductor`, `exists_leadingCoeff_pow_smul_mem_radical_conductor`, `isIntegral_of_isIntegralElem_of_monic_of_natDegree_lt`, `isStronglyTranscendental_mk_radical_conductor`	23
Total	24

Algebra

Definitions

Name	Category	Theorems
`ZariskisMainProperty` 📖	MathDef	6 math math: `zariskisMainProperty_iff`, `ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt`, `ZariskisMainProperty.of_isIntegral`, `zariskisMainProperty_iff'`, `zariskisMainProperty_iff_exists_saturation_eq_top`, `ZariskisMainProperty.of_finiteType`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_isStronglyTranscendental_of_quasiFiniteAt` 📖	mathematical	—	`IsStronglyTranscendental`	—	`not_isStronglyTranscendental_of_weaklyQuasiFiniteAt` `WeaklyQuasiFiniteAt.instOfQuasiFiniteAt`
`not_isStronglyTranscendental_of_weaklyQuasiFiniteAt` 📖	mathematical	—	`IsStronglyTranscendental`	—	`Function.Injective.isDomain` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `FractionRing.instFaithfulSMul` `IsScalarTower.subalgebra'` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `subset_adjoin` `IsScalarTower.to_smulCommClass` `Subalgebra.instIsScalarTowerSubtypeMem` `Commute.all` `AlgHom.range_eq_top` `Subalgebra.map_injective` `Subtype.val_injective` `map_top` `le_antisymm` `Set.image_subset_range` `Subalgebra.range_val` `Set.image_congr` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `one_mul` `Localization.isLocalization` `IsScalarTower.subalgebra` `Subalgebra.instFaithfulSMulSubtypeMem` `Module.FaithfullyFlat.faithfulSMul` `Module.FaithfullyFlat.instOfNontrivialOfFree` `FractionRing.instNontrivial` `IsDomain.toNontrivial` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `IsDomain.to_noZeroDivisors` `instIsDomain` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `NoZeroDivisors.toNoZeroSMulDivisors` `integralClosure.isIntegralClosure` `Ideal.exists_minimalPrimes_le` `bot_le` `Ideal.instIsTwoSided_1` `Ideal.map_isPrime_of_surjective` `Ideal.Quotient.mk_surjective` `Ideal.mk_ker` `WeaklyQuasiFiniteAt.of_surjectiveOnStalks` `RingHom.surjectiveOnStalks_of_surjective` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Ideal.comap_map_of_surjective` `WeaklyQuasiFiniteAt.of_restrictScalars` `Ideal.Quotient.isScalarTower_of_liesOver` `Ideal.over_under` `isReduced_of_noZeroDivisors` `Ideal.Quotient.noZeroDivisors` `RingHom.Finite.of_comp_finite` `Polynomial.ringHom_ext'` `RingHom.ext` `Polynomial.map_C` `Polynomial.aeval_C` `Polynomial.map_X` `Polynomial.aeval_X` `RingHom.Finite.comp` `RingHom.Finite.of_surjective` `Ideal.Quotient.isDomain` `Ideal.Quotient.instFaithfulSMul` `IsStronglyTranscendental.of_surjective_left` `isStronglyTranscendental_mk_of_mem_minimalPrimes`
`quasiFiniteAt_iff_isOpen_singleton_fiber` 📖	mathematical	—	`QuasiFiniteAt` `PrimeSpectrum.asIdeal` `CommRing.toCommSemiring` `PrimeSpectrum.isPrime` `IsOpen` `Set.Elem` `PrimeSpectrum` `Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `Set.instMembership` `PrimeSpectrum.zariskiTopology`	—	`PrimeSpectrum.isPrime` `Homeomorph.isOpen_image` `Set.image_singleton` `to_smulCommClass` `QuasiFiniteAt.baseChange` `Homeomorph.symm_apply_apply` `IsClopen.isOpen` `QuasiFiniteAt.isClopen_singleton` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `IsLocalRing.ResidueField.finite_of_module_finite` `IsIntegral.isLocalHom` `IsPurelyInseparable.isIntegral` `isPurelyInseparable_self` `Module.FaithfullyFlat.faithfulSMul` `Module.FaithfullyFlat.instOfNontrivialOfFree` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Module.Free.self` `Module.Finite.self` `FiniteType.baseChange` `QuasiFiniteAt.of_isOpen_singleton_fiber`
`zariskisMainProperty_iff` 📖	mathematical	—	`ZariskisMainProperty` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsIntegral` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Function.Bijective.eq_1` `IsLocalization.map_injective_of_injective` `Subtype.val_injective` `IsLocalization.Away.instMapRingHomPowersOfCoe` `Localization.isLocalization` `Localization.awayMap_surjective_iff`
`zariskisMainProperty_iff'` 📖	mathematical	—	`ZariskisMainProperty` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsIntegral` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`zariskisMainProperty_iff` `IsIntegral.pow_iff` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `pow_succ`
`zariskisMainProperty_iff_exists_saturation_eq_top` 📖	mathematical	—	`ZariskisMainProperty` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Subalgebra.saturation` `integralClosure` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`instIsConcreteLE`

Algebra.QuasiFiniteAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_fg_and_exists_notMem_and_awayMap_bijective` 📖	mathematical	—	`Submodule.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `Ideal` `SetLike.instMembership` `Submodule.setLike` `Semiring.toModule` `Subalgebra.instSetLike` `Function.Bijective` `Localization.Away` `CommSemiring.toCommMonoid` `Subalgebra.toCommSemiring` `RingHom` `RingHom.instFunLike` `AlgHom.toRingHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `Subalgebra.val` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `Localization.awayMap`	—	`Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective` `Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt`
`of_isOpen_singleton_fiber` 📖	mathematical	`IsOpen` `Set.Elem` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `Set.instMembership` `PrimeSpectrum.zariskiTopology`	`Algebra.QuasiFiniteAt` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime`	—	`PrimeSpectrum.isPrime` `Algebra.to_smulCommClass` `of_isOpen_singleton` `instIsArtinianOfIsSemisimpleModuleOfFinite` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `IsLocalRing.ResidueField.finite_of_module_finite` `Algebra.IsIntegral.isLocalHom` `IsPurelyInseparable.isIntegral` `isPurelyInseparable_self` `Module.FaithfullyFlat.faithfulSMul` `Module.FaithfullyFlat.instOfNontrivialOfFree` `IsLocalRing.toNontrivial` `Localization.AtPrime.isLocalRing` `Module.Free.self` `Module.Finite.self` `Algebra.FiniteType.baseChange` `Set.image_singleton` `Homeomorph.isOpen_image` `of_quasiFiniteAt_residueField` `PrimeSpectrum.instLiesOverAsIdealComapAlgebraMap` `RingHom.instRingHomClass` `Homeomorph.symm_apply_apply`
`of_quasiFiniteAt_residueField` 📖	mathematical	`Ideal.comap` `Ideal.Fiber` `RingHom` `TensorProduct` `CommRing.toCommSemiring` `Ideal.ResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Algebra.toModule` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `AlgHom.toRingHom` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `RingHom.instRingHomClass`	`Algebra.QuasiFiniteAt`	—	`RingHom.instRingHomClass` `Algebra.to_smulCommClass` `Algebra.WeaklyQuasiFiniteAt.of_quasiFiniteAt_residueField` `of_weaklyQuasiFiniteAt`
`of_weaklyQuasiFiniteAt` 📖	mathematical	—	`Algebra.QuasiFiniteAt`	—	`Algebra.ZariskisMainProperty.quasiFiniteAt` `Algebra.ZariskisMainProperty.of_finiteType_of_weaklyQuasiFiniteAt`

Algebra.ZariskisMainProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_fg_and_exists_notMem_and_awayMap_bijective` 📖	mathematical	`Algebra.ZariskisMainProperty`	`Submodule.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `Ideal` `SetLike.instMembership` `Submodule.setLike` `Semiring.toModule` `Subalgebra.instSetLike` `Function.Bijective` `Localization.Away` `CommSemiring.toCommMonoid` `Subalgebra.toCommSemiring` `RingHom` `RingHom.instFunLike` `AlgHom.toRingHom` `Subalgebra.toSemiring` `Subalgebra.algebra` `Subalgebra.val` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `Localization.awayMap`	—	`Algebra.FiniteType.out` `Algebra.subset_adjoin` `fg_adjoin_of_finite` `Set.Finite.image` `Finset.finite_toSet` `IsLocalization.map_injective_of_injective` `Subtype.val_injective` `IsLocalization.Away.instMapRingHomPowersOfCoe` `Localization.isLocalization` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Algebra.map_top` `Subalgebra.map_le` `Algebra.adjoin_le_iff` `Set.mem_insert_of_mem` `mul_comm` `pow_mem` `SubsemiringClass.toSubmonoidClass` `Subalgebra.instSubsemiringClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Function.Surjective.exists` `IsLocalization.mk'_surjective` `IsLocalization.map_mk'` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsLocalization.eq_iff_exists` `IsLocalization.exists_mk'_eq` `map_mul` `map_pow` `Submonoid.instSubmonoidClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsScalarTower.coe_toAlgHom` `Localization.mk_eq_mk'` `IsLocalization.mk'.congr_simp` `one_pow` `IsLocalization.smul_mk'_one` `Algebra.zariskisMainProperty_iff`
`of_finiteType` 📖	mathematical	—	`Algebra.ZariskisMainProperty`	—	`of_finiteType_of_weaklyQuasiFiniteAt` `Algebra.WeaklyQuasiFiniteAt.instOfQuasiFiniteAt`
`of_finiteType_of_weaklyQuasiFiniteAt` 📖	mathematical	—	`Algebra.ZariskisMainProperty`	—	`Algebra.FiniteType.iff_quotient_mvPolynomial''` `small_of_surjective` `MvPolynomial.instSmall` `UnivLE.small` `UnivLE.self` `univLE_of_max` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `Algebra.WeaklyQuasiFiniteAt.comap_algEquiv` `AlgHom.Finite.of_surjective` `AlgEquiv.surjective` `Algebra.zariskisMainProperty_iff'` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquiv.apply_symm_apply` `IsIntegral.map` `IsScalarTower.left` `AlgHom.algHomClass`
`of_isIntegral` 📖	mathematical	—	`Algebra.ZariskisMainProperty`	—	`Algebra.zariskisMainProperty_iff'` `Submonoid.one_mem` `Algebra.IsIntegral.isIntegral`
`quasiFiniteAt` 📖	mathematical	`Algebra.ZariskisMainProperty`	`Algebra.QuasiFiniteAt`	—	`exists_fg_and_exists_notMem_and_awayMap_bijective` `Submodule.fg_top` `Algebra.QuasiFinite.trans` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Algebra.QuasiFinite.instOfFinite` `Algebra.QuasiFinite.instLocalization` `Module.Finite.self` `Algebra.QuasiFinite.of_surjective_algHom` `Localization.isLocalization` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsUnit.pow` `IsLocalization.map_units` `Algebra.QuasiFinite.of_forall_exists_mul_mem_range` `IsLocalization.exists_mk'_eq` `AlgHom.commutes`
`restrictScalars` 📖	—	`Algebra.ZariskisMainProperty`	—	—	`Algebra.zariskisMainProperty_iff'` `isIntegral_trans`
`trans` 📖	—	`Algebra.ZariskisMainProperty` `Ideal.under` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Subalgebra.saturation` `Bot.bot` `Subalgebra` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	—	—	`Algebra.zariskisMainProperty_iff'` `Algebra.zariskisMainProperty_iff` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.IsPrime.mul_notMem` `Ideal.IsPrime.mem_of_pow_mem` `Ideal.IsPrime.under` `Eq.ge` `Set.mem_univ` `pow_add` `mul_pow` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `IsIntegral.algebraMap` `IsIntegral.mul` `IsIntegral.pow`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range` 📖	mathematical	`RingHom.IsIntegralElem` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `CommRing.toRing` `AlgHom.toRingHom` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AlgHom` `AlgHom.funLike`	`IsIntegral` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.toSMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.leadingCoeff`	—	`IsScalarTower.right` `IsScalarTower.of_algebraMap_eq` `IsLocalization.map_eq` `IsScalarTower.algebraMap_apply` `OreLocalization.instIsScalarTower` `IsLocalization.Away.algebraMap_isUnit` `Localization.isLocalization` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.ringHom_ext'` `RingHom.ext` `Polynomial.aeval_map_algebraMap` `AlgHom.commutes` `Polynomial.map_X` `Polynomial.aeval_X` `exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range` `Polynomial.Monic.map` `Polynomial.eval₂_map` `Polynomial.hom_eval₂` `AlgHom.toRingHom_eq_coe` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Polynomial.Monic.leadingCoeff` `Polynomial.leadingCoeff_C_mul_of_isUnit` `Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero` `IsUnit.ne_zero` `IsUnit.val_inv_mul` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Polynomial.aeval_C` `Polynomial.aeval_algebraMap_apply` `Polynomial.aeval_algHom_apply` `Polynomial.aeval_X_left` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_assoc` `IsLocalization.integerNormalization_map_to_map` `Algebra.smul_def` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `map_sub` `RingHomClass.toAddMonoidHomClass` `IsIntegral.mul` `isIntegral_algebraMap` `IsIntegral.exists_multiple_integral_of_isLocalization` `IsLocalization.exists_isIntegral_smul_of_isIntegral_map` `IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero`
`exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range` 📖	mathematical	`RingHom.IsIntegralElem` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `CommRing.toRing` `AlgHom.toRingHom` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Polynomial.Monic` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AlgHom` `AlgHom.funLike`	`IsIntegral` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`eq_or_ne` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `one_mul` `sub_self` `isIntegral_of_isIntegralElem_of_monic_of_natDegree_lt` `RingHom.IsIntegralElem.sub` `RingHom.isIntegralElem_map` `Polynomial.natDegree_modByMonic_lt` `mul_sub` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `Polynomial.modByMonic_add_div`
`exists_leadingCoeff_pow_smul_mem_conductor` 📖	mathematical	`integralClosure` `Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `conductor` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.X` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Algebra.toSMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.leadingCoeff`	—	`IsScalarTower.of_algebraMap_eq'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `Polynomial.adjoin_X` `Algebra.map_top` `exists_isIntegral_leadingCoeff_pow_smul_sub_of_isIntegralElem_of_mul_mem_range` `RingHom.Finite.to_isIntegral` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Eq.le` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.commutes` `sub_add_cancel` `Module.Finite.fg_top` `AlgHom.map_adjoin_singleton` `Algebra.smul_mul_assoc` `Submodule.span_induction` `Finset.le_sup` `pow_add` `SemigroupAction.mul_smul` `Subalgebra.smul_mem` `MulZeroClass.mul_zero` `smul_zero` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `mul_add` `Distrib.leftDistribClass` `smul_add` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `mul_smul_comm` `Algebra.to_smulCommClass` `SMulCommClass.smul_comm` `IsScalarTower.to_smulCommClass` `Algebra.smul_def` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `AlgHom.mem_range_self` `Eq.ge` `Set.mem_univ`
`exists_leadingCoeff_pow_smul_mem_radical_conductor` 📖	mathematical	`integralClosure` `Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.radical` `conductor` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.X` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Algebra.toSMul` `Polynomial.coeff`	—	`exists_leadingCoeff_pow_smul_mem_conductor` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mul_pow` `smul_pow` `IsScalarTower.right` `Algebra.to_smulCommClass` `zero_smul` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `pow_add` `add_comm` `mul_smul_mul_comm` `IsScalarTower.left` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `pow_mul` `Polynomial.leadingCoeff_pow'` `Nat.strong_induction_on` `lt_or_ge` `Polynomial.coeff_eq_zero_of_natDegree_lt` `Nat.instCanonicallyOrderedAdd` `eq_or_ne` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.commutes` `sub_mul` `mul_right_comm` `Algebra.smul_def` `sub_mem` `Submodule.addSubgroupClass` `Polynomial.eraseLead_coeff` `LE.le.trans_lt` `Polynomial.eraseLead_natDegree_le` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `Nat.instZeroLEOneClass`
`isIntegral_of_isIntegralElem_of_monic_of_natDegree_lt` 📖	mathematical	`RingHom.IsIntegralElem` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.commRing` `CommRing.toRing` `AlgHom.toRingHom` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Polynomial.Monic` `Polynomial.natDegree` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AlgHom` `AlgHom.funLike`	`IsIntegral`	—	`Localization.isLocalization` `mul_comm` `IsLocalization.Away.mul_invSelf` `subsingleton_or_nontrivial` `RingHom.codomain_trivial` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `isIntegral_zero` `le_integralClosure_iff_isIntegral` `Algebra.adjoin_le_iff` `Set.singleton_subset_iff` `SetLike.mem_coe` `mem_integralClosure_iff` `Algebra.self_mem_adjoin_singleton` `Polynomial.Monic.sub_of_left` `Polynomial.Monic.map` `Polynomial.degree_lt_degree` `lt_imp_lt_of_le_of_le` `Polynomial.natDegree_C_mul_le` `le_refl` `Polynomial.natDegree_map_le` `Polynomial.Monic.natDegree_map` `Polynomial.eval₂_sub` `Polynomial.aeval_map_algebraMap` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Polynomial.aeval_algebraMap_apply` `OreLocalization.instIsScalarTower` `Polynomial.aeval_algHom_apply` `AlgHom.algHomClass` `Polynomial.aeval_X_left` `Polynomial.eval₂_mul` `Polynomial.eval₂_C` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_right_comm` `one_mul` `sub_self` `isIntegral_trans` `Subalgebra.isScalarTower_mid` `IsScalarTower.left` `AlgHomClass.toRingHomClass` `AlgHom.toRingHom_eq_coe` `Polynomial.eval₂_map` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Polynomial.hom_eval₂` `Polynomial.ringHom_ext'` `RingHom.ext` `AlgHom.commutes` `Polynomial.aeval_X` `IsLocalization.Away.isIntegral_of_isIntegral_map` `isIntegral_of_isIntegral_adjoin_of_mul_eq_one`
`isStronglyTranscendental_mk_radical_conductor` 📖	mathematical	`integralClosure` `Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`IsStronglyTranscendental` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.radical` `conductor` `Ideal.Quotient.commRing` `Ideal.instAlgebraQuotient` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	`Ideal.instIsTwoSided_1` `Function.Surjective.forall` `Ideal.Quotient.mk_surjective` `Polynomial.ext` `Polynomial.coeff_mul_C` `Polynomial.coeff_map` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Polynomial.aeval_X` `Algebra.smul_def` `exists_leadingCoeff_pow_smul_mem_radical_conductor` `Ideal.Quotient.eq_zero_iff_mem` `map_mul` `Ideal.Quotient.algebraMap_eq` `Polynomial.aeval_algebraMap_apply` `Ideal.Quotient.isScalarTower` `IsScalarTower.right`

---

← Back to Index