Theorems · Theorem · ring theory

AddOreLocalization.cardinalMk_le_lift_cardinalMk_of_addCommute

∀ {R : Type u} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type v)
  [inst_2 : AddAction R X],
  (∀ (s s' : ↥S), AddCommute s s') → Cardinal.mk (AddOreLocalization S X) ≤ Cardinal.lift.{u, v} (Cardinal.mk X)

Defined in

Mathlib.GroupTheory.OreLocalization.Cardinality

Cited by

0 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidAddOreLocalization.AddOreSetAddAction