decidablePred — Mathlib

English

The predicate IsSquare is decidable on any finite type α with a multiplication and decidable equality.

Русский

Предикат IsSquare разрешим на любом конечном множестве α с умножением иDecidableEq.

LaTeX

$$$\\\\text{DecidablePred}(\text{IsSquare} : \\alpha \\to \\text{Prop}) \\\\text{ for all } [Mul \\alpha] [Fintype \\alpha] [DecidableEq \\alpha].$$$

Lean4

instance decidablePred [Mul α] [Fintype α] [DecidableEq α] : DecidablePred (IsSquare : α → Prop) := fun _ =>
  Fintype.decidableExistsFintype

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