add_div'

Mathlib.Algebra.Field.Basic

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

English

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

Русский

Для a,b,c в K и c ≠ 0 выполняется b + a/c = (bc + a)/c.

LaTeX

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

Lean4

theorem add_div' (a b c : K) (hc : c ≠ 0) : b + a / c = (b * c + a) / c := by rw [add_div, mul_div_cancel_right₀ _ hc]

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

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

Разделы

Аффилиация

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