taylorEquiv_symm

Mathlib.Algebra.Polynomial.Taylor

URI: https://scilib.ai/kg/mathlib#Polynomial.taylorEquiv_symm

English

The symm of TaylorEquiv r equals TaylorEquiv(-r).

Русский

Обратное отображение для TaylorEquiv r равно TaylorEquiv(-r).

LaTeX

$$$$ (\\mathrm{taylorEquiv}(r)).\\mathrm{symm} = \\mathrm{taylorEquiv}( -r ). $$$$

Lean4

@[simp]
theorem taylorEquiv_symm : (taylorEquiv r).symm = taylorEquiv (-r) :=
  AlgEquiv.ext fun _ ↦ rfl

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

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

Разделы

Аффилиация

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