Documentation
Mathlib
.
RingTheory
.
OreLocalization
.
Cardinality
Search
return to top
source
Imports
Init
Mathlib.GroupTheory.OreLocalization.Cardinality
Mathlib.RingTheory.OreLocalization.Ring
Imported by
OreLocalization
.
cardinalMk
Cardinality of Ore localizations of rings
#
This file contains some results on cardinality of Ore localizations of rings.
source
theorem
OreLocalization
.
cardinalMk
{R :
Type
u}
[
Ring
R
]
{S :
Submonoid
R
}
[
OreSet
S
]
(hS :
S
≤
nonZeroDivisorsRight
R
)
:
Cardinal.mk
(
OreLocalization
S
R
)
=
Cardinal.mk
R