fintypeRangeS — Mathlib

English

If R is finite and S has decidable equality, then the rangeS of any ring hom f: R → S is a finite type.

Русский

Если множество R конечное и в S задано разрешимое равенство, то образ rangeS(f) имеет конечный тип.

LaTeX

$$$ [Fintype\ R] \rightarrow [DecidableEq\ S] \rightarrow Fintype (rangeS\ f) $$$

Lean4

/-- The range of a morphism of semirings is a fintype, if the domain is a fintype.
Note: this instance can form a diamond with `Subtype.fintype` in the
  presence of `Fintype S`. -/
instance fintypeRangeS [Fintype R] [DecidableEq S] (f : R →+* S) : Fintype (rangeS f) :=
  Set.fintypeRange f

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