div_div_cancel_left

Mathlib.Algebra.Group.Units.Basic

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

← MathLib Explorer

English

If a is a unit, then a / b / a = b^{-1}.

Русский

Если a является единицей, то a / b / a = b^{-1}.

LaTeX

$$$$ \\forall a \\in \\alpha^{\\times},\\ b \\in \\alpha:\\ \\frac{a}{b a} = \\frac{1}{b}. $$$$

Lean4

@[to_additive]
protected theorem div_div_cancel_left (h : IsUnit a) : a / b / a = b⁻¹ := by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]

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

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

Разделы

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

Аффилиация

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