decidableMemZPowers — Mathlib

English

There is a (noncomputable in general) instance giving a decision procedure for membership in zpowers(a).

Русский

Существует (в общем случае не вычислимый) экземпляр, дающий решение для принадлежности к zpowers(a).

LaTeX

$$$ \text{DecidablePred } (x \in zpowers(a)) $$$

Lean4

@[to_additive] -- TODO: delete?

noncomputable instance decidableMemZPowers {a : G} : DecidablePred (· ∈ Subgroup.zpowers a) :=
  Classical.decPred _

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