instDecidableEqQuotientSubgroupOfDecidablePredMem

Mathlib.GroupTheory.Coset.Defs

URI: https://scilib.ai/kg/mathlib#QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem

English

If membership in s is decidable, then equality on α / s is decidable.

Русский

Если членство в s разрешимо, то равенство на α / s разрешимо.

LaTeX

$$[DecidablePred (x ∈ s)] ⇒ [DecidableEq (α / s)]$$

Lean4

@[to_additive]
instance [DecidablePred (· ∈ s)] : DecidableEq (α ⧸ s) :=
  @Quotient.decidableEq _ _ (leftRelDecidable _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru