cardinalMk — Mathlib

English

If S is a localization of R at M and M consists of non-zero divisors, then the localizations have the same cardinality as R.

Русский

Если S локализация R по M, и M состоит из ненулевых делителей, кардинальности локализации равны кардинальности R.

LaTeX

$$$\\#(\\mathrm{Localization}\\, S) = \\#R$$$

Lean4

theorem cardinalMk {S : Submonoid R} (hS : S ≤ R⁰) : #(Localization S) = #R :=
  by
  apply OreLocalization.cardinalMk
  rwa [nonZeroDivisorsLeft_eq_nonZeroDivisors]

Похожие утверждения