instDecidableEq — Mathlib

English

Units α have decidable equality whenever α has decidable equality.

Русский

Единицы α имеют разрешимое равенство тогда и только тогда, когда у α есть разрешимое равенство.

LaTeX

$$$$ \\operatorname{DecidableEq}(\\alpha^{\\times}) \\text{ given } \\operatorname{DecidableEq}(\\alpha). $$$$

Lean4

/-- Units have decidable equality if the base `Monoid` has decidable equality. -/
@[to_additive /-- Additive units have decidable equality
    if the base `AddMonoid` has decidable equality. -/
    ]
instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ Units.ext_iff

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