eq_div_of_mul_eq_right

Mathlib.Algebra.EuclideanDomain.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.eq_div_of_mul_eq_right

English

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

Русский

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

LaTeX

$$$ a \neq 0 \to (a * b = c) \Rightarrow b = c / a $$$

Lean4

theorem eq_div_of_mul_eq_right {a b c : R} (ha : a ≠ 0) (h : a * b = c) : b = c / a := by
  rw [← h, mul_div_cancel_left₀ _ ha]

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

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

Разделы

Аффилиация

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