one_notMem_inv_mul_iff

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.one_notMem_inv_mul_iff

English

(1) ∉ t^{-1} * s iff Disjoint s t.

Русский

(1) ∉ t^{-1} * s тогда и только тогда, когда s и t несовпадают.

LaTeX

$$(1 ∉ t^{-1} * s) ⇔ Disjoint(s,t)$$

Lean4

@[to_additive]
theorem one_notMem_inv_mul_iff : (1 : α) ∉ t⁻¹ * s ↔ Disjoint s t :=
  one_mem_inv_mul_iff.not_left

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

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

Разделы

Аффилиация

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