div_add'

Mathlib.Algebra.Field.Basic

URI: https://scilib.ai/kg/mathlib#div_add'

English

For a,b,c ∈ K with c ≠ 0, a = (a + bc)/c − b.

Русский

Для a,b,c ∈ K с c ≠ 0 верно a = (a + bc)/c − b.

LaTeX

$$$$a = \frac{a + b c}{c} - b \quad(c\neq 0).$$$$

Lean4

theorem div_add' (a b c : K) (hc : c ≠ 0) : a / c + b = (a + b * c) / c := by rwa [add_comm, add_div', add_comm]

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

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

Разделы

Аффилиация

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