Cardinality

📁 Source: Mathlib/RingTheory/Localization/Cardinality.lean

Statistics

Metric	Count
Definitions	0
Theorems mk_fractionRing, cardinalMk, cardinalMk, lift_cardinalMk, cardinalMk, cardinalMk_le, lift_cardinalMk, lift_cardinalMk_le, cardinalMk	9
Total	9

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_fractionRing 📖	mathematical	—	FractionRing	—	IsLocalization.cardinalMk Localization.isLocalization le_rfl

FractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk 📖	mathematical	—	FractionRing	—	Cardinal.mk_fractionRing

IsFractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk 📖	—	—	—	—	IsLocalization.cardinalMk le_rfl
lift_cardinalMk 📖	mathematical	—	Cardinal.lift	—	IsLocalization.lift_cardinalMk le_rfl

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk 📖	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	—	—	Cardinal.lift_id lift_cardinalMk
cardinalMk_le 📖	mathematical	—	Cardinal Cardinal.instLE	—	Cardinal.lift_id lift_cardinalMk_le
lift_cardinalMk 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	Cardinal.lift	—	Localization.cardinalMk Cardinal.lift_mk_eq'
lift_cardinalMk_le 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift	—	Localization.cardinalMk_le Cardinal.lift_mk_eq' Cardinal.lift_le

Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	Localization CommRing.toCommMonoid	—	OreLocalization.cardinalMk nonZeroDivisorsLeft_eq_nonZeroDivisors

---

← Back to Index