mul_sub_div_right

Mathlib.Algebra.EuclideanDomain.Basic

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

← MathLib Explorer

English

If z ≠ 0 and z ∣ y, then (x·z − y)/z = x − y/z.

Русский

Если z ≠ 0 и z делит y, то (x·z − y)/z = x − y/z.

LaTeX

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

Lean4

theorem mul_sub_div_right (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (x * z - y) / z = x - y / z :=
  by
  rw [mul_comm x z]
  exact mul_sub_div_left _ _ _ h1 h2

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

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

Разделы

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

Аффилиация

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