mul_div_mul_cancel

Mathlib.Data.EReal.Inv

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

← MathLib Explorer

English

Let a, b, c ∈ EReal with c ≠ ⊥, ⊤ and c ≠ 0. Then (a · c) / (b · c) = a / b.

Русский

Пусть a, b, c ∈ EReal, c не равен ⊥, ⊤ и c ≠ 0. Тогда (a · c) / (b · c) = a / b.

LaTeX

$$$\dfrac{a c}{b c} = \dfrac{a}{b}$$$

Lean4

theorem mul_div_mul_cancel (h₁ : c ≠ ⊥) (h₂ : c ≠ ⊤) (h₃ : c ≠ 0) : a * c / (b * c) = a / b := by
  rw [← mul_div_right a (b * c) c, ← div_div a b c, div_mul_cancel h₁ h₂ h₃]

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

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

Разделы

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

Аффилиация

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