mul_div_cancel

Mathlib.Data.EReal.Inv

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

English

Let a, b ∈ EReal with b not bottom, not top, and b ≠ 0. Then b · (a / b) = a.

Русский

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

LaTeX

$$$b \cdot (a / b) = a$$$

Lean4

theorem mul_div_cancel (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : b * (a / b) = a := by
  rw [mul_comm, div_mul_cancel h₁ h₂ h₃]

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

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

Разделы

Аффилиация

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