fintypeFieldRange — Mathlib

English

If the domain K is finite, then the subfield f.fieldRange is finite (as a type).

Русский

Если область определения K конечна, то подполе f.fieldRange конечно по количеству элементов.

LaTeX

$$$\lvert f.fieldRange \rvert < \infty$$$

Lean4

/-- The range of a morphism of fields is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with `Subtype.Fintype` if `L` is also a fintype. -/
instance fintypeFieldRange [Fintype K] [DecidableEq L] (f : K →+* L) : Fintype f.fieldRange :=
  Set.fintypeRange f

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