add_mul_div_right

Mathlib.Algebra.EuclideanDomain.Basic

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

← MathLib Explorer

English

If y ≠ 0 and y ∣ x, then (x + z·y)/y = x/y + z (с правой стороны).

Русский

Если y ≠ 0 и y делит x, то (x + z·y)/y = x/y + z (с правой стороны).

LaTeX

$$$ (x + z \cdot y)/y = x/y + z $$$

Lean4

theorem add_mul_div_right (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x + z * y) / y = x / y + z :=
  by
  rw [mul_comm z y]
  exact add_mul_div_left _ _ _ h1 h2

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

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

Разделы

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

Аффилиация

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