eq_div_of_mul_eq''

Mathlib.Algebra.Group.Basic

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

English

If b = c / a then a b = c.

Русский

Если b = c / a, то a b = c.

LaTeX

$$$\forall a,b,c\in G,\ b = c / a \Rightarrow a b = c$$$

Lean4

@[to_additive eq_sub_of_add_eq']
theorem eq_div_of_mul_eq'' (h : c * a = b) : a = b / c := by simp [h.symm]

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

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

Разделы

Аффилиация

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