aevalDifferentialEquiv_apply

Mathlib.RingTheory.Extension.Presentation.Submersive

URI: https://scilib.ai/kg/mathlib#Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply

English

For any x, applying aevalDifferentialEquiv to x equals applying aevalDifferential to x.

Русский

Для любого x применение aevalDifferentialEquiv к x равно применению aevalDifferential к x.

LaTeX

$$$\\operatorname{aevalDifferentialEquiv}(P)\\, x = \\operatorname{aeval}(P)\\, x$$$

Lean4

@[simp]
theorem aevalDifferentialEquiv_apply [Finite σ] (x : σ → S) : P.aevalDifferentialEquiv x = P.aevalDifferential x :=
  rfl

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

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

Разделы

Аффилиация

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