decidableMemRange — Mathlib

English

If G is finite and N has decidable equality, then membership in the range of a monoid hom f: G →* N is decidable.

Русский

Если G конечна и N имеет разрешимое равенство, то для моноидного гомоморфизма f : G →* N множество учащегося f(G) вычислимо.

LaTeX

$$$f:\,G\to^* N,\; [Fintype\ G],\; [DecidableEq\ N]\; \Rightarrow\; DecidablePred(\cdot \in f.range)$$$

Lean4

@[to_additive]
instance decidableMemRange (f : G →* N) [Fintype G] [DecidableEq N] : DecidablePred (· ∈ f.range) := fun _ =>
  Fintype.decidableExistsFintype

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