Algebra

📁 Source: Mathlib/RingTheory/Artinian/Algebra.lean

Statistics

Metric	Count
Definitions	0
Theorems isUnit_iff_nonZeroDivisor_of_isIntegral, isUnit_iff_nonZeroDivisor_of_isIntegral', isUnit_of_isIntegral_of_nonZeroDivisor, isUnit_of_nonZeroDivisor_of_isIntegral', isUnit_submonoid_eq_of_isIntegral	5
Total	5

IsArtinianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_iff_nonZeroDivisor_of_isIntegral 📖	mathematical	IsIntegral	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	IsUnit.mem_nonZeroDivisors isUnit_of_isIntegral_of_nonZeroDivisor
isUnit_iff_nonZeroDivisor_of_isIntegral' 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	isUnit_iff_nonZeroDivisor_of_isIntegral Algebra.IsIntegral.isIntegral
isUnit_of_isIntegral_of_nonZeroDivisor 📖	mathematical	IsIntegral Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Ring.toSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	IsUnit MonoidWithZero.toMonoid	—	Algebra.self_mem_adjoin_singleton Subtype.val_injective comap_nonZeroDivisors_le_of_injective RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass isUnit_of_mem_nonZeroDivisors isArtinian_of_tower IsScalarTower.right isArtinian_of_fg_of_artinian' Algebra.finite_adjoin_simple_of_isIntegral
isUnit_of_nonZeroDivisor_of_isIntegral' 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Ring.toSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	IsUnit MonoidWithZero.toMonoid	—	isUnit_of_isIntegral_of_nonZeroDivisor Algebra.IsIntegral.isIntegral
isUnit_submonoid_eq_of_isIntegral 📖	mathematical	—	IsUnit.submonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring nonZeroDivisors	—	Submonoid.ext isUnit_iff_nonZeroDivisor_of_isIntegral'

---

← Back to Index