invFun_add

Mathlib.RingTheory.PolynomialAlgebra

URI: https://scilib.ai/kg/mathlib#PolyEquivTensor.invFun_add

English

invFun is additive: invFun(p + q) = invFun(p) + invFun(q).

Русский

invFun аддитивна: invFun(p + q) = invFun(p) + invFun(q).

LaTeX

$$invFun\\_R A(p+q) = invFun\\_R A(p) + invFun\\_R A(q)$$

Lean4

@[simp]
theorem invFun_add {p q} : invFun R A (p + q) = invFun R A p + invFun R A q := by simp only [invFun, eval₂_add]

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

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

Разделы

Аффилиация

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