instDecidableEqRingFunc — Mathlib

English

The symbols of the language of rings form a finite type with exactly five symbols: add, mul, neg, zero, one.

Русский

Символы языка кольца образуют конечный тип, состоящий из пяти символов: сложение, умножение, отрицание, нуль и единица.

LaTeX

$$$\text{card }\text{Language.ring.Symbols} = 5.$$$

Lean4

instance instDecidableEqRingFunc {a✝} : DecidableEq✝ (@FirstOrder.ringFunc✝ a✝) :=
  instDecidableEqRingFunc.decEq

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