cardinalMk — Mathlib

English

If S is contained in the left zero divisors of R, then the cardinality of the Ore localization equals the cardinality of R: |OreLocalization(S,R)| = |R|.

Русский

Если S содержится в левым нулевым делителям R, то кардинал локализации Ора равен кардиналу R: |OreLocalization(S,R)| = |R|.

LaTeX

$$( S \le nonZeroDivisorsLeft(R) ) ⇒ \lvert OreLocalization(S,R) \rvert = \lvert R \rvert$$

Lean4

theorem cardinalMk (hS : S ≤ nonZeroDivisorsLeft R) : #(OreLocalization S R) = #R :=
  le_antisymm (cardinalMk_le S) (mk_le_of_injective (numeratorHom_inj hS))

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