one_notMem_div_iff — Mathlib

English

For any subsets s, t of a group α, 1 is not in s / t if and only if s and t are disjoint.

Русский

Для любых подмножеств s, t группы α 1 не принадлежит s / t тогда и только тогда, когда s и t непересекаются.

LaTeX

$$$ (1 : \alpha) \notin s / t \iff s \cap t = \emptyset $$$

Lean4

@[to_additive]
theorem one_notMem_div_iff : (1 : α) ∉ s / t ↔ Disjoint s t :=
  one_mem_div_iff.not_left

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