Cardinality of Ore localizations of rings

This file contains some results on cardinality of Ore localizations of rings.

theorem OreLocalization.cardinalMk {R : Type u} [Ring R] {S : Submonoid R} [OreSet S] (hS : S ≤ nonZeroDivisorsLeft R) : Cardinal.mk (OreLocalization S R) = Cardinal.mk R