div_eq_iff_eq_mul'

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#div_eq_iff_eq_mul'

English

Let G be a commutative group. For all a, b, c ∈ G, a / b = c iff a = b · c.

Русский

Пусть G — коммутативная группа. Для любых a, b, c ∈ G верно: a / b = c ⇔ a = b · c.

LaTeX

$$$\\dfrac{a}{b} = c \\iff a = b \\cdot c$$$

Lean4

@[to_additive]
theorem div_eq_iff_eq_mul' : a / b = c ↔ a = b * c := by rw [div_eq_iff_eq_mul, mul_comm]

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

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

Разделы

Аффилиация

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