mul_div_mul_right_eq_div

Mathlib.Algebra.Group.Basic

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

← MathLib Explorer

English

For all a,b,c ∈ G, (a c) / (b c) = a / b.

Русский

Для любых a,b,c ∈ G выполняется (a c) / (b c) = a / b.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mul_div_mul_right_eq_div (a b c : G) : a * c / (b * c) = a / b := by rw [div_mul_eq_div_div_swap];
  simp only [mul_div_cancel_right]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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