LocalRing

📁 Source: Mathlib/RingTheory/AdicCompletion/LocalRing.lean

Statistics

Metric	Count
Definitions	0
Theorems isLocalRing_of_isAdicComplete_maximal, isUnit_iff_notMem_of_isAdicComplete_maximal	2
Total	2

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalRing_of_isAdicComplete_maximal 📖	mathematical	—	IsLocalRing CommSemiring.toSemiring CommRing.toCommSemiring	—	Ideal.zero_mem Ideal.ne_top_iff_one Ideal.IsMaximal.ne_top isUnit_iff_notMem_of_isAdicComplete_maximal Ideal.add_mem
isUnit_iff_notMem_of_isAdicComplete_maximal 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsUnit.exists_left_inv Ideal.mul_mem_left Ideal.ne_top_iff_one Ideal.IsMaximal.ne_top IsScalarTower.right Ideal.instIsTwoSided_1 zero_add pow_one Iff.not Ideal.Quotient.eq_zero_iff_mem factorPowSucc.isUnit_of_isUnit_image IsScalarTower.left Ideal.IsTwoSided.instHPowNat Ideal.Quotient.mk_surjective Ideal.mul_top SModEq.sub_mem map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MulZeroClass.mul_zero mul_sub Ideal.pow_le_pow_right map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_comm map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass sub_self pow_zero Ideal.one_eq_top IsAdicComplete.toIsPrecomplete sub_zero sub_add_cancel map_add AddMonoidHomClass.toAddHomClass SModEq.symm isUnit_iff_exists_inv' instIsDedekindFiniteMonoid sub_eq_zero IsHausdorff.haus IsAdicComplete.toIsHausdorff

---

← Back to Index