pderiv_def — Mathlib

English

pderiv i is equal to mkDerivation R (Pi.single i 1) when a decidable equality on σ exists.

Русский

Если существует разрешимое равенство на σ, то pderiv i равен mkDerivation R (Pi.single i 1).

LaTeX

$$$$ [\\text{DecidableEq}(\\sigma)] \\Rightarrow pderiv(i) = \\mathrm{mkDerivation}(R, \\Pi.single(i,1)). $$$$

Lean4

theorem pderiv_def [DecidableEq σ] (i : σ) : pderiv i = mkDerivation R (Pi.single i 1) := by unfold pderiv; congr!

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