fintypeRange — Mathlib

English

If the domain R is finite and S has decidable equality, then the range of f is a finite type.

Русский

Если область определения R конечна и для S задано решение эквивалентности, то образ f является конечным множеством типов.

LaTeX

$$$[Fintype R] \\ [DecidableEq S] \\Rightarrow Fintype (\\mathrm{range}(f))$$$

Lean4

/-- The range of a ring homomorphism 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 fintypeRange [Fintype R] [DecidableEq S] (f : R →+* S) : Fintype (range f) :=
  Set.fintypeRange f

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