OreSet

📁 Source: Mathlib/RingTheory/OreLocalization/OreSet.lean

Statistics

Metric	Count
Definitions OreSet, oreSetOfCancelMonoidWithZero, oreSetOfIsCancelMulZero, oreSetOfNoZeroDivisors	4
Theorems nonempty_oreSet_iff, nonempty_oreSet_iff_of_noZeroDivisors	2
Total	6

OreLocalization

Definitions

Name	Category	Theorems
OreSet 📖	CompData	3 math math: nonempty_oreSet_iff_of_noZeroDivisors, nonempty_oreSet_iff, nonempty_oreSet_of_strongRankCondition
oreSetOfCancelMonoidWithZero 📖	CompOp	—
oreSetOfIsCancelMulZero 📖	CompOp	—
oreSetOfNoZeroDivisors 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_oreSet_iff 📖	mathematical	—	OreSet MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Submonoid SetLike.instMembership Submonoid.instSetLike	—	ore_right_cancel ore_eq
nonempty_oreSet_iff_of_noZeroDivisors 📖	mathematical	—	OreSet MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike	—	ore_eq

---

← Back to Index