decidableMemKer — Mathlib

English

If M has decidable equality, membership in the kernel is decidable by checking f(x) = 1.

Русский

Если у M есть разрешимое равенство, принадлежность ядру решаема через проверку f(x) = 1.

LaTeX

$$$$ \\text{DecidablePred}(x \\in \\ker f) \\iff (f(x) = 1) $$$$

Lean4

@[to_additive]
instance decidableMemKer [DecidableEq M] (f : G →* M) : DecidablePred (· ∈ f.ker) := fun x =>
  decidable_of_iff (f x = 1) f.mem_ker

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