derivation_eq_of_forall_mem_vars — Mathlib

English

Two derivations are equal if they agree on all X_i for every i in σ.

Русский

Две производные равны, если они согласованы на всех X_i для каждого i в σ.

LaTeX

$$$\\\\forall D_1 D_2, \\\\forall i, D_1(X_i) = D_2(X_i) \\\\Rightarrow \\\\ D_1 = D_2$$$

Lean4

theorem derivation_eq_of_forall_mem_vars {D₁ D₂ : Derivation R (MvPolynomial σ R) A} {f : MvPolynomial σ R}
    (h : ∀ i ∈ f.vars, D₁ (X i) = D₂ (X i)) : D₁ f = D₂ f :=
  derivation_eqOn_supported h f.mem_supported_vars

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