mul_eq_of_eq_div'

Mathlib.Algebra.Group.Basic

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

English

If h : a / b = c, then a * b = c.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_eq_of_eq_div' (h : b = c / a) : a * b = c := by rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]

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

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

Разделы

Аффилиация

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