add_div_eq_mul_add_div

Mathlib.Algebra.Field.Basic

URI: https://scilib.ai/kg/mathlib#add_div_eq_mul_add_div

← MathLib Explorer

English

For a in K and c ≠ 0, a/c + b = (ac + b)/c.

Русский

Для a,b,c в K и c ≠ 0 верно a/c + b = (ac + b)/c.

LaTeX

$$$$a/c + b = (a\cdot c + b)/c \quad (c\neq 0).$$$$

Lean4

theorem add_div_eq_mul_add_div (a b : K) (hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
  (eq_div_iff_mul_eq hc).2 <| by rw [right_distrib, div_mul_cancel₀ _ hc]

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

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

Разделы

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

Аффилиация

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