mul_div_mul_left

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#IsUnit.mul_div_mul_left

← MathLib Explorer

English

In a DivisionCommMonoid, for unit c, c·a / (c·b) = a / b for all a,b.

Русский

В DivisionCommMonoid, для единицы c, c·a / (c·b) = a / b для всех a,b.

LaTeX

$$$\forall {\alpha} [DivisionCommMonoid\ \alpha] {c} IsUnit c \forall (a b : \alpha), (c\cdot a)/(c\cdot b) = a/b$$$

Lean4

@[to_additive]
protected theorem mul_div_mul_left (h : IsUnit c) (a b : α) : c * a / (c * b) = a / b := by
  rw [mul_comm c, mul_comm c, h.mul_div_mul_right]

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

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

Разделы

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

Аффилиация

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