GoingDown

📁 Source: Mathlib/RingTheory/IntegralClosure/GoingDown.lean

Statistics

Metric	Count
Definitions	0
Theorems coeff_mem_radical_span_coeff_of_dvd, instHasGoingDownOfIsDomainOfFaithfulSMulOfIsIntegralOfIsIntegrallyClosed	2
Total	2

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_mem_radical_span_coeff_of_dvd 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.radical Ideal.span setOf natDegree coeff	—	Ideal.radical_eq_sInf Ideal.mem_sInf Ideal.instIsTwoSided_1 ext lt_trichotomy coeff_map coeff_X_pow LT.lt.ne Ideal.subset_span Monic.leadingCoeff map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coeff_eq_zero_of_natDegree_lt map_zero MonoidWithZeroHomClass.toZeroHomClass LT.lt.ne' dvd_prime_pow instIsCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsDomain.toIsCancelMulZero Ideal.Quotient.isDomain prime_X map_dvd isUnit_iff Ideal.Quotient.noZeroDivisors Units.isUnit X_pow_mul_C coeff_C_mul MulZeroClass.mul_zero natDegree_mul_X_pow IsDomain.toNontrivial IsUnit.ne_zero natDegree_C zero_add Monic.natDegree_map Units.eq_mul_inv_iff_mul_eq

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasGoingDownOfIsDomainOfFaithfulSMulOfIsIntegralOfIsIntegrallyClosed 📖	mathematical	—	Algebra.HasGoingDown	—	Function.Injective.isDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective Algebra.smul_def Ideal.comap.congr_simp IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower IsScalarTower.right IsLocalization.mem_map_algebraMap_iff Localization.isLocalization NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.exists_monic_aeval_eq_zero_forall_mem_of_mem_map Ideal.instIsTwoSided_1 Polynomial.ext lt_trichotomy Polynomial.coeff_map Polynomial.coeff_X_pow LT.lt.ne Mathlib.Tactic.Push.not_and_eq Polynomial.Monic.leadingCoeff minpoly.monic Algebra.IsIntegral.isIntegral map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass Polynomial.coeff_eq_zero_of_natDegree_lt map_zero MonoidWithZeroHomClass.toZeroHomClass LT.lt.ne' map_pow AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.aeval_X Polynomial.aeval_map_algebraMap Ideal.Quotient.tower_quotient_map_quotient Polynomial.aeval_algebraMap_apply Ideal.Quotient.isScalarTower minpoly.aeval Ideal.IsPrime.mem_of_pow_mem Ideal.map_le_iff_le_comap LT.lt.le Ideal.Quotient.eq_zero_iff_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Polynomial.coeff_mem_radical_span_coeff_of_dvd minpoly.isIntegrallyClosed_dvd FaithfulSMul.to_isTorsionFree IsDomain.toNontrivial IsDomain.toIsCancelMulZero Ideal.IsPrime.mem_or_mem IsIntegrallyClosed.minpoly_smul Polynomial.natDegree_scaleRoots Ideal.radical_eq_sInf Polynomial.coeff_scaleRoots Ideal.comap_map_eq_self_iff_of_isPrime LE.le.antisymm Ideal.le_comap_map LE.le.trans_eq Localization.AtPrime.isLocalRing Ideal.comap_mono IsLocalRing.le_maximalIdeal_of_isPrime Localization.AtPrime.comap_maximalIdeal Ideal.IsPrime.under Ideal.under_under

---

← Back to Index