mk_fractionRing — Mathlib

English

The cardinality of the fraction field (fraction ring) of a commutative ring R equals the cardinality of R.

Русский

Кардинальность дробной кольцевой локализации (поле дробей) кольца R равна кардинальности R.

LaTeX

$$$\\#(\\mathrm{FractionRing}\\,R) = \\#R$$$

Lean4

@[simp]
theorem mk_fractionRing (R : Type u) [CommRing R] : #(FractionRing R) = #R :=
  IsLocalization.cardinalMk (FractionRing R) R⁰ le_rfl

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