polynomialEquiv_symm

Mathlib.RingTheory.Kaehler.Polynomial

URI: https://scilib.ai/kg/mathlib#KaehlerDifferential.polynomialEquiv_symm

English

The inverse of polynomialEquiv is given by P times D(X).

Русский

Обратная система polynomialEquiv задаётся как P·D(X).

LaTeX

$$$(polynomialEquiv\\;R)^{-1}(P) = P \\cdot D\\;R\\;R[X](X).$$$

Lean4

@[simp]
theorem polynomialEquiv_symm (P) : (polynomialEquiv R).symm P = P • D R R[X] X :=
  rfl

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

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

Разделы

Аффилиация

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