decidableEq — Mathlib

English

If α is a commutative monoid with cancellation and α has decidable equality, then Localization S has decidable equality; i.e., equality in Localization S can be decided using a decidable equality on α.

Русский

Пусть α — коммутативный моноид с отменой и имеет разрешимость равенств; тогда локализация Localization S также имеет разрешимость равенств: равенство элементов локализации можно решить, пользуясь разрешимостью равенств в α.

LaTeX

$$$\\text{DecidableEq}(\\text{Localization } S)$$$

Lean4

@[to_additive]
instance decidableEq [DecidableEq α] : DecidableEq (Localization s) := fun a b =>
  Localization.recOnSubsingleton₂ a b fun _ _ _ _ => decidable_of_iff' _ mk_eq_mk_iff'

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