finSuccEquiv_X_succ

Mathlib.Algebra.MvPolynomial.Equiv

URI: https://scilib.ai/kg/mathlib#MvPolynomial.finSuccEquiv_X_succ

English

For any j in Fin n, finSuccEquiv(R,n)(X j.succ) equals C(X j).

Русский

Для каждого j ∈ Fin n верно: finSuccEquiv(R,n)(X j.succ) = C(X j).

LaTeX

$$$\\forall j : \\mathrm{Fin}(n), \\; \\operatorname{finSuccEquiv} \\; R \\; n (X j.succ) = \\operatorname{Polynomial}.C( X j )$$$

Lean4

theorem finSuccEquiv_X_succ {j : Fin n} : finSuccEquiv R n (X j.succ) = Polynomial.C (X j) := by
  simp [finSuccEquiv_apply]

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

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

Разделы

Аффилиация

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