mem_divPairs

Mathlib.GroupTheory.MonoidLocalization.DivPairs

URI: https://scilib.ai/kg/mathlib#Submonoid.mem_divPairs

English

An element x = (m1,m2) belongs to divPairs f s if and only if f(m1)/f(m2) ∈ s.

Русский

Элемент x = (m1,m2) принадлежит divPairs f s тогда и только тогда, когда f(m1)/f(m2) ∈ s.

LaTeX

$$x ∈ divPairs f s ↔ f(x.1)/f(x.2) ∈ s$$

Lean4

@[to_additive (attr := simp)]
theorem mem_divPairs : x ∈ divPairs f s ↔ f x.1 / f x.2 ∈ s :=
  .rfl

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

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

Разделы

Аффилиация

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