mul_eq_of_eq_div

Mathlib.Algebra.Group.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_eq_of_eq_div (h : a = c / b) : a * b = c := by simp [h]

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

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

Разделы

Аффилиация

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