mul_div_mul_cancel

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.mul_div_mul_cancel

← MathLib Explorer

English

If a ≠ 0, then (a · b) / (a · c) = b / c.

Русский

Если a ≠ 0, то (a · b) / (a · c) = b / c.

LaTeX

$$$a \\\\neq 0 \\\\Rightarrow (a \\\\cdot b) \\\\\\div (a \\\\cdot c) = b / c$$$

Lean4

theorem mul_div_mul_cancel {a : Ordinal} (ha : a ≠ 0) (b c) : a * b / (a * c) = b / c :=
  by
  convert mul_add_div_mul (Ordinal.pos_iff_ne_zero.2 ha) b c using 1
  rw [add_zero]

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

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

Разделы

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

Аффилиация

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