IntegrallyClosed

📁 Source: Mathlib/Algebra/GCDMonoid/IntegrallyClosed.lean

Statistics

Metric	Count
Definitions	0
Theorems toIsIntegrallyClosed, surj_of_gcd_domain	2
Total	2

GCDMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsIntegrallyClosed 📖	mathematical	—	IsIntegrallyClosed	—	isIntegrallyClosed_iff Localization.isLocalization IsLocalization.surj_of_gcd_domain Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero IsFractionRing.injective mul_comm isUnit_iff_dvd_one one_pow Dvd.dvd.trans dvd_gcd dvd_refl gcd_pow_left_dvd_pow_gcd pow_dvd_pow_of_dvd map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Units.coe_map_inv Units.eq_mul_inv_iff_mul_eq

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surj_of_gcd_domain 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring GCDMonoid.gcd CommSemiring.toCommMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	exists_mk'_eq extract_gcd mul_comm mul_mk'_eq_mk'_of_mul mk'_mul_cancel_left

---

← Back to Index