fintype' — Mathlib

English

The localization of a finite ring is finite; there exists a finite-type structure on S when R is finite.

Русский

Локализация конечного кольца остаётся конечным; существует конечная структура над S, когда R конечно.

LaTeX

$$$|R| < \\infty \\Rightarrow |S| < \\infty$$$

Lean4

/-- The localization of a `Fintype` is a `Fintype`. Cannot be an instance. -/
noncomputable def fintype' [Fintype R] : Fintype S :=
  have := Classical.propDecidable
  Fintype.ofSurjective (Function.uncurry <| IsLocalization.mk' S) fun a =>
    Prod.exists'.mpr <| IsLocalization.mk'_surjective M a

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