Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

Regular Paper

可換環の微分の形式化とその応用
Derivation of Commutative Ring and its Application
渡瀬 泰成 1,*
Yasushige Watase1,*
1 東京都杉並区
1 Suginami-ku, Tokyo, Japan* yasushige.watase@gmail.com
Proof checked by Mizar Version: 8.1.10 and MML Version: 5.63.1382
Received: December 9, 2020. Accepted: April 30, 2021.

Abstract
A derivation of Polynomial over R has formalized in [1] and a polynomial was regarded a real differentiable function. In this article we treat more algebraic aspect about
derivation rather than analytic case. A derivation is defined for a commutative ring A
as a map D : A −→ A satisfying D(x + y) = Dx + DyD(xy) = xDy + yDx ∀x, y ∈ A [2].
Form the definition various properties of a derivation are derived axiomatic way. In thearticle most formalized theorems are on to polynomial ring. Because generic theory israther simpler than polynomial ring case, it is worth to investigate polynomial case forfurther formalization. There is a certain difficulty in handling with polynomial rings due
to an element of the rings has 2 deferent attributes namely ‘Polynomial’ and ‘Elementof the carrier of the ring’. The article formalized a finite sequence of polynomial andproperties of a derivation of a polynomial ring. We also formalized Leibnitz Formulafor power of derivation of R[X] as example of justification of the current work :Dn (xy) =

n ( )
∑
n
i=0

1

i

Dn−i xDi y.

はじめに
本稿では, 環の微分を考慮して一変数多項式環 (以下多項式環と記す) の微分とその性質を述べ, 応用として多項式の積の高階微分のライプニッツの公式の形式化を論じた. まず環の微分を定義する.

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

1/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

定義 1 A を可換環とし, 写像 D : A −→ A が以下をみたすとき D を A の微分という．

D(x + y) = Dx + Dy, D(xy) = xDy + yDx ∀x, y ∈ A.と記述される. 恒等零写像は微分の条件を満たす. 恒等零でない具体的な環の微分としては多項式環の微分が挙げられる. これには先行して形式化 [1] がライブラリにある．この形式化は実係数の多項式 p に対して以下の様に形式化されている. しかしながら積の微分は形式化されていない．

Listing 1. POLYDIFFA - Def.5
deﬁnition
let p;
func poly diﬀ(p) −> sequence of F Real means:: POLYDIFF:def 5
for n being Nat holds it.n = p.(n+1) ∗ (n+1);
end;

これに対して可換環上の多項式環の微分で微分の次数をパラメータとして持つ定義をあたえた. 実多項式の形式微分を任意のこの定義では微分は多項式環から多項式環への写像は定義できない．属性 Polynomial を多項式環の元として扱うことができないことによる. 写像の構成には多項式環の元は属性 Element of the carrier of Polynom-Ring としなければならないが本稿は既存ライブラリと互換性を確保するため POLYDIFF-Def.5 と同様の定義とした．

Listing 2. POLYDIFFA- Def.3
deﬁnition
let R;
let f be Polynomial of R;
let r be Nat;func D (f,r) −> sequence of R means
POLYDIFFA:def 3
for i being Nat holds it.i = In((i+r)!/(i!),R) ∗ f.(i+r) ;end;

この定義は既存アーティクル [1] の定義と互換性があり, 多項式の積の微分がライプニッツ則を満たすことが証明される.

Listing 3. POLYDIFFA - Th10&Th31
theorem :: POLYDIFFA:10
for f be Polynomial of F Real holds D (f,1) = poly diﬀ(f);D1ｆ ()は D (f,1)の再定義である．
theorem :: POLYDIFFA:31
D1(f∗’g) = (D1(f))∗’g + f∗’(D1(g));
proof
per cases;
suppose that
A1: f is non constant;thus thesis by A1,Th28;
end;
suppose that
A2: f is constant;thus thesis by A2,Th27;
end;
end;ここで

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

2/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

Th27,は以下の如し：Th28
theorem :: POLYDIFFA:29
theorem Th27:
for p, q be Polynomial of F Realst p is constant holds D1(p∗’q) = (D1(p))∗’q + p∗’(D1(q))
theorem :: POLYDIFFA:30
theorem Th28:
for x,y be Polynomial of F Real st x is non constantholds D1(x∗’y) = (D1(x))∗’y + x∗’(D1(y))

2多項式環の微分の性質の形式化

2.1

基本的な性質の形式化

任意の可換環で微分 D の満たす性質は FM 誌に “RINGDER1” にて形式化した.

i) D(1. R) = 0. R&D(0. R) = 0. Rii) D(nx) = nD(x)iii) Dx(n+1) = (n + 1)xm Dxiv) Dn+1 x = D(Dn x)
以下が上記 i）-iv) の多項式に対応した形式化となる.

Listing 4. POLYDIFFA - Th12-15
theorem :: POLYDIFFA:12
D1(0 .F Real) = 0 .F Real;
theorem :: POLYDIFFA:13
for n,m be Nat, f be Polynomial of F Real holds
In(n,F Real)∗f + In(m,F Real)∗f = In(n+m,F Real)∗f;theorem :: POLYDIFFA:14
D (f,r) is Polynomial of F Real;
theorem :: POLYDIFFA:15
D1(D (f,r)) = D (f,r+1);2.2多項式の微分の公式例

次数 d の多項式 f の 0 次から d 次微分の和は次を満たす.

D(f (0) + f (1) + f (2) + · · · + f (d) ) + f = (f (0) + f (1) + f (2) + · · · + f (d) )(1)

この証明概要は任意の多項式の有限列 F に対してその各要素の微分をとる操作を定義し得られる結果を D(F ) と表記する.

長さ d+1 の多項式の有限列 ⟨f (0) , f (1) , · · · , f (d) ⟩ を

HWZ(f) として定義する. d + 1 番目の成分は微分すると D(f (d+1) ) = 恒等 0 写像 となる．
有限列 D(HWZ(f)) の成分と HWZ(f) を比較し和を取り証明される. 形式化では多項式のMMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

3/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

有限列は定義出来ないので, Polynomial 属性から Element of the carrier of Polynom-Ringの元への変換関数を定義し多項式 f の多項式環の元のとして表示するときˆf と表現する.

HWZ(f) は ⟨ ˆf (0) , · · · , ˆf (d) ⟩ として扱う．Polynomial 属性から Element of the carrierof Polynom-Ring の元への変換と逆変換の関数を導入する.
定義 2 可換環 A の多項式環を Polynom-Ring A とする．Polynom-Ring A の多項式 fの Element of the carrier of Polynom-Ring A の元への属性の対応をˆf と表記する．

Element of the carrier of Polynom-Ring A の元 x を多項式の属性に変換したときは, 変換後の表記を˜x とする.
上記の定義を踏まえて HWZ(f) は以下の様に定義する.

Listing 5. POLYDIFFA - Def.5
deﬁnition
let f be Polynomial of F Real;func HWZ(f) −> FinSequence of the carrier of Polynom−Ring F Real means:: POLYDIFFA:def 5
len it = len f & for i be Nat st i in dom it holds
it.i = ˆ(D (f,i −’ 1));end;

the carrier of Polynom-Ring A の元の有限列の総和は既存のライブラリから導入される. しかしながら多項式の有限集合への微分は新規に定義する必要がある.

Listing 6. POLYDIFFA - Def.7
deﬁnition
let S be FinSequence of the carrier of Polynom−Ring F Real;func D1(S) −> FinSequence of Polynom−Ring F Real means:: POLYDIFFA:def 7
len it = len S & for i be Nat st i in dom it holds
it.i = ˆD1(˜(S/.i));end;

以上の準備の下, 等式 (1) の形式化は以下の如し,

Listing 7. POLYDIFFA - Th39
theorem :: POLYDIFFA:39
for f be non constant Polynomial of F Real holds
˜Sum(HWZ(f)) = D1(˜Sum(HWZ(f))) + f;

2.3

高次冪のライプニッツの公式の形式化

高次冪のライプニッツの公式はよく知られた次の公式である.
n ( )
∑
n
n
D (f g) =Dn−i f Di g.
ii=0

この公式をどのように形式的に表現するのか具体的にパスカルの図を作り D1 (f g), D2 (f g) · · ·( )から公式の形式的な構成を考察する．公式の右辺の項 ni Dn−i f Di g を成分とする長さ

n + 1 の有限列を考え, それを LBZ と名付け以下の通りに形式化する. FinSequence の引数は集合の元を要請するので FinSequence of Polynomial とは出来ない.

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

4/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

Listing 8. POLYDIFFA - Def.8
deﬁnition
let n;
let x,y be Element of the carrier of Polynom−Ring F Real;func LBZ(n,x,y) −> FinSequence of the carrier of Polynom−Ring F Real means:: POLYDIFFA:def 8
len it = n+1 & for i st i in dom it holds
it.i = ˆ(In(n choose (i−’1),F Real)∗((D (˜x,n+1−’i))∗’(D (˜y,i −’ 1))));
end;

この有限列 Dn (f g) = Sum(LBZ(D, n, x, y) 帰納法にて証明し以下の定理を得る. 以下の定理は FM 誌 “RINGDER1” にて形式化した微分の定理の実数上 1 変数の多項式環に対応する形式化であり今後形式化を予定.

Listing 9. RINGDER1 - Th25
theorem Th25:(D|ˆn).(x∗y) = Sum(LBZ(D,n,x,y))theorem :: RINGDER1:25(D|ˆn).(x∗y) = Sum(LBZ(D,n,x,y));

証明は LBZ(D, n, x, y) は

( n)i

Dn−i f Di g に対応している. 但し形式化では添え字のずれを補正している. ここでは非形式での証明及び図１のパスカルの図との対応を示し形式表現( )の読解の補いとしたい. LBZ1 と LBZ2 は組み合わせの数の分解の部分 ni Dn−i f Di g =( ) ( n ) n−i( ni + i+1)D f Di+1 g と変形したときの二つの項の和を二つの項にして有限列にし,この組み合わせの数の分解の前半, 後半の項で生成できる列の先頭と末尾の項を除いて奇数項、偶数項をとってそれぞれ LBZ1 と LBZ2 部分列に分けている. これらを準備して帰∑n ( )
納法で LBZ(D, n, x, y) = i=0 ni Dn−i f Di g が n の時成り立てば n + 1 でも成り立つことを証明する．計算手順は Σ 記号の添え字と項の式変形の計算で形式表現可能と考えられるがここではパスカルの図の手順にならっている.

Listing 10. POLYDIFFA - Def.9-11
deﬁnition
let m;
let x,y be Element of Polynom−Ring F Real;func LBZ0(m,x,y) −> FinSequence of the carrier of Polynom−Ring F Real means:: POLYDIFFA:def 9
len it = m & for i st i in dom it holds
it.i =ˆ(In((m choose (i−’1))+(m choose i),F Real)∗((D (˜x,m+1 −’i))∗’(D (˜y,i))));
end;
deﬁnition
let m;
let x,y be Element of the carrier of Polynom−Ring F Real;func LBZ1(m,x,y) −> FinSequence of the carrier of Polynom−Ring F Real means:: POLYDIFFA:def 10
len it = m &for i st i in dom it holds
it.i = ˆ(In(m choose (i−’1),F Real)∗((D (˜x,m+1 −’i))∗’(D (˜y,i))));
end;
deﬁnition
let m;
let x,y be Element of the carrier of Polynom−Ring F Real;func LBZ2(m,x,y) −> FinSequence of the carrier of Polynom−Ring F Real means:: POLYDIFFA:def 11
len it = m &for i st i in dom it holds

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

5/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

it.i = ˆ(In(m choose i,F Real)∗((D (˜x,m +1 −’i))∗’(D (˜y,i))));
end;

f(0) g(0)f g(1)

f(1) g

LBZ(1)

f(2) gD.LBZ(1)に現れる項LBZ1(1)f(1) g(1)f(1) g(1)

LBZ1(1).1
LBZ2(1).1

LBZ2(1)
LBZ0(1)

2f(1) g(1)

LBZ(2)
D.LBZ(2)2f(1) g(1)f(2) gf(3) gf(2) g(1)2f(2) g(1)f g(2)
2f(1) g(2)

LBZ2(2).1

LBZ2(2)
LBZ0(2)f(3) gf(1) g(2)f g(3)

LBZ1(2).2

LBZ1(2).1

LBZ1(2)

LBZ(3)

f g(2)

LBZ2(2).2

3f(2) g(1)3f(1) g(2)3f(2) g(1)3f(1) g(2)f g(3)

図 1. 多項式 f,g の微分のパスカルの図. f (i) , g (j) はそれぞれ f, g の i 次,j 次の微分を表す. LBZはライプニッツ公式に現れる項を与える多項式の有限列.

3

形式化の課題と展望
多項式の微分に関する定理を形式化する場合, 証明の記述の途中で属性の変換が発生, 証明自体分かりにくいものとなる. 多項式に関するライブラリの既存資源は多項式をPolynomial 属性で扱って居り多項式環の元から出発した定義との親和性が低い点が課題といえる. 2.2 節の定義２の属性変換を利用せざる得なかった. 今回は R[X] の多項式を主に扱ったが一般の可換環係数の多項式環でも同様に形式化できる. 但し多項式に整数を乗ずる場合で係数環の有限標数では扱い異なる. 今回の形式化により多項式とその微分を伴った定理群の証明が可能となるのでその応用は広い. 更なる発展としては有理関数体の微分やべき級数, ローラン級数の微分などが見込まれる.

参考文献[1] Kornilowicz A. Differentiability of Polynomials over Reals. Formalized Mathematics.
2017;25(1):31–37.

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

6/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)[2] Matsumura H. Commutative Ring Theory. 2nd ed. Cambridge Studies in Advanced
Mathematics. Cambridge University Press; 1989.

Mizar article information
Works in Progress
POLYDIFFA Properties of Modules over a Commutative Ringby Yasushige Watase
Summary: A derivation of Polynomial over R has formalized in [1] and a polynomial
was regarded a real differentiable function. In this article we treat more algebraic aspect
about derivation rather than analytic case. A derivation is defined for a commutative
ring A as a map D : A −→ A satisfying D(x+y) = Dx+DyD(xy) = xDy +yDx ∀x, y ∈A [2]. Form the definition various properties of a derivation are derived axiomatic way.
In the article most formalized theorems are on to polynomial ring. Because generictheory is rather simpler than polynomial ring case, it is worth to investigate polynomialcase for further formalization. There is a certain difficulty in handling with polynomial
rings due to an element of the rings has 2 deferent attributes namely ‘Polynomial’ and‘Element of the carrier of the ring’. The article formalized a finite sequence of polynomial
and properties of a derivation of a polynomial ring. We also formalized Leibnitz Formulafor power of derivation of R[X] as example of justification of the current work :n

D (xy) =

n ( )
∑
n
i=0

i

Dn−i xDi y.

Listing 11. POLYDIFFA - abstract
environvocabularies VECTSP 1, POLYNOM1, PARTFUN1, NUMBERS, REAL 1, RELAT 1, TARSKI,
STRUCT 0, FUNCT 1, SUBSET 1, ALGSEQ 1, NAT 1, XXREAL 0, SUPINF 2, INT 3,
POLYNOM3, ARYTM 3, CARD 1, FUNCT 7, MESFUNC1, FINSEQ 1, INT 1, XBOOLE 0,
HURWITZ, ARYTM 1, AFINSQ 1, REALSET1, CARD 3, ORDINAL4, XCMPLX 0, C0SP1,
POLYDIFF, FINSEQ 3, FIELD 1, RFINSEQ, RATFUNC1, XREAL 0, RAT 1, GAUSSINT,POLYNOM5, VECTSP 2, FOMODEL1, ALGSTR 0, ZFMISC 1, FINSEQ 2, FINSEQ 5,
POLYDIFA;
notations TARSKI, XBOOLE 0, ZFMISC 1,SUBSET 1, RELAT 1, FUNCT 1, ORDINAL1,
RELSET 1, PARTFUN1, FUNCT 2, BINOP 1, FUNCT 3, FUNCOP 1, NUMBERS,XCMPLX 0, XXREAL 0, XREAL 0, NAT 1, INT 1, RAT 1, VALUED 0, INT 2, NAT D,
FINSEQ 1, FINSEQ 2, NEWTON, RFINSEQ, FINSEQ 5, STRUCT 0, ALGSTR 0,
RLVECT 1, VECTSP 1, COMPLFLD, GROUP 1, FUNCSDOM, VECTSP 2, GROUP 4,NORMSP 1, VFUNCT 1, FVSUM 1, POLYNOM1, ALGSEQ 1, POLYNOM3, POLYNOM5,
UPROOTS, INT 3, HURWITZ, C0SP1, EC PF 1, RATFUNC1, GAUSSINT, RING 3,
RING 4, POLYDIFF, FIELD 1, FIELD 4;
constructors TARSKI, XBOOLE 0, ZFMISC 1, SUBSET 1, RELAT 1, FUNCT 1, ORDINAL1,
RELSET 1, PARTFUN1, FUNCT 2, BINOP 1, FUNCT 3, REALSET1, XCMPLX 0,
FINSET 1, NUMBERS, SQUARE 1, NAT 1, INT 1, RAT 1, INT 2, NAT D, BINOP 2,
NEWTON, RFINSEQ, FINSEQ 5, FUNCT 7, STRUCT 0, ALGSTR 0, RLVECT 1,
VECTSP 1, GROUP 1, COMPLFLD,VECTSP 2, VFUNCT 1, GROUP 4, FVSUM 1, POLYNOM1, ALGSEQ 1, BINOM,POLYNOM3, POLYNOM4, POLYNOM5, UPROOTS, INT 3, C0SP1, VECTSP11, EC PF 1,
RATFUNC1, GAUSSINT, RING 3, POLYDIFF, FIELD 1, FIELD 4;

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

7/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

registrations RELSET 1, FUNCT 2, VECTSP 1, STRUCT 0, XBOOLE 0, RELAT 1,
FUNCT 1, NAT 1, XREAL 0, NUMBERS, XCMPLX 0, ORDINAL1, POLYNOM3, MEMBERED,FUNCOP 1, RATFUNC1, INT 1, POLYNOM5, FINSEQ 1, VALUED 1, VALUED 0,
FDIFF 1, RCOMP 1, POLYNOM4, RLVECT 1, XXREAL 0, ALGSTR 1, POLYDIFF,
RING 4, AFINSQ 1, NEWTON, GAUSSINT, COMPLFLD, RAT 1, INT 3, FIELD 4,
RING 5, FINSEQ 5;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
deﬁnitions TARSKI, FUNCT 1, FUNCT 2, FDIFF 1, ALGSEQ 1, RATFUNC1, XBOOLE 0,
RELAT 1, RELAT 2, RLVECT 1, GROUP 1, VECTSP 1, ALGSTR 0;
equalities SUBSET 1, STRUCT 0, ALGSTR 0, VECTSP 1, POLYNOM3, HURWITZ,POLYNOM5, FUNCSDOM, VALUED 1, FINSEQ 1, XCMPLX 0, POLYDIFF, RLVECT 1,
RATFUNC1, BINOP 1, FINSEQ 2, XBOOLE 0, NUMBERS, XREAL 0, INT 3, COMPLEX1,
RING 4, FUNCOP 1, SQUARE 1, PARTFUN1;
expansions FDIFF 1, ALGSEQ 1, FUNCT 1, POLYNOM1, NUMBERS,STRUCT 0, VECTSP 1, TARSKI, FUNCT 2, FINSEQ 1, RING 4, RFINSEQ,RATFUNC1, POLYDIFF, RLVECT 1, GROUP 1, SUBSET 1,XREAL 0, NORMSP 1,
SQUARE 1, XBOOLE 0, VECTSP 2, IDEAL 1;
theorems FUNCT 2, POLYNOM5, UPROOTS, FINSEQ 5, ORDINAL1, XREAL 0, ALGSEQ 1,
XXREAL 0, XREAL 1, NAT 1, RATFUNC1, HURWITZ, INT 1, FINSEQ 1, FINSEQ 3,
RLVECT 1, NORMSP 1, PARTFUN1, NAT D, FVSUM 1, POLYNOM4, NEWTON, POLYNOM3,
POLYDIFF, XCMPLX 1, BINOM, RING 4, RFINSEQ, FIELD 1, RING 5, FUNCT 1,
SUBSET 1, FINSEQ 2, FINSEQ 4, PRE POLY, TARSKI, INT 3, FIELD 4, C0SP1,
POLYALG1, VECTSP 2, POLYNOM1, FUNCT 3, ZFMISC 1;
schemes FUNCT 2, NAT 1, FINSEQ 1;
begin :: Preliminaries
reserve R1 for non degenerated comRing;
reserve R for (INT.Ring)−extending comRing;
reserve c for Complex;
reserve x0,r for Real;reserve i,j,k, m,n,d,r for Nat;
reserve x,y,z for Element of the carrier of Polynom−Ring F Real;registration
cluster F Real −> (INT.Ring)−extending;end;
registration
let R;
let i be Integer;
reduce In(i,R) to i;end;reserve f for Element of the carrier of Polynom−Ring R;
theorem :: POLYDIFFA:1
for p be Polynomial of R holds p‘ˆn is Polynomial of R;
deﬁnition
let R1;
let p be Element of the carrier of Polynom−Ring R1;
func ˜p −> Polynomial of R1 means:: POLYDIFFA:def 1
it is Polynomial of R1 & it = p;end;
deﬁnition
let R1;
let p be Polynomial of R1;
func ˆp −> Element of the carrier of Polynom−Ring R1
means

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

8/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.):: POLYDIFFA:def 2
it is Element of the carrier of Polynom−Ring R1 & it = p;
end;theorem :: POLYDIFFA:2
for p,q be Polynomial of R1 holds ˆ(p+q) = (ˆp) + (ˆq);
theorem :: POLYDIFFA:3
for p be Element of the carrier of Polynom−Ring R1 holds ˆ(˜p) = p;theorem :: POLYDIFFA:4
for p be Polynomial of R1 holds ˜(ˆp) = p;theorem :: POLYDIFFA:5
for p,q be Element of Polynom−Ring R holds
˜(p+q) = (˜p) + (˜q);
theorem :: POLYDIFFA:6
for p,q be Element of the carrier of Polynom−Ring R holds(p+q) = (˜p) + (˜q);
theorem :: POLYDIFFA:7
for p,q be Element of Polynom−Ring R holds
˜(p∗q) = (˜p) ∗’ (˜q);
theorem :: POLYDIFFA:8
for p,q be Polynomial of R1 holds ˆ(p∗’q) = (ˆp) ∗ (ˆq);
theorem :: POLYDIFFA:9
for p,q be Polynomial of F Real holds ˆ(p∗’q) = (ˆp) ∗ (ˆq);
deﬁnition
let R;
let f be Polynomial of R;
let r be Nat;func D (f,r) −> sequence of R means:: POLYDIFFA:def 3
for i being Nat holds it.i = In((i+r)!/(i!),R) ∗ f.(i+r) ;end;
registration
let R;
let f be Polynomial of R;
let r be Nat;cluster D (f,r) −> ﬁnite−Support;
end;
theorem :: POLYDIFFA:10
for f be Polynomial of F Real holds
D (f,1) = poly diﬀ(f);deﬁnition
let f be Polynomial of F Real;func D1(f) −> Polynomial of F Real equals:: POLYDIFFA:def 4
poly diﬀ(f);end;reserve f for Polynomial of F Real;
theorem :: POLYDIFFA:11
D (f,0) = f;theorem :: POLYDIFFA:12
D1(0 .F Real) = 0 .F Real;MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

9/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

theorem :: POLYDIFFA:13
for n,m be Nat, f be Polynomial of F Real holds
In(n,F Real)∗f + In(m,F Real)∗f = In(n+m,F Real)∗f;theorem :: POLYDIFFA:14
D (f,r) is Polynomial of F Real;
theorem :: POLYDIFFA:15
D1(D (f,r)) = D (f,r+1);
theorem :: POLYDIFFA:16
for f be non constant Polynomial of F Real holds
deg f >= 1 & len f >= 2 & len f = deg f + 1 & len f−’1 = len f −1 &len f > 1;
reserve p for Polynomial of F Real;reserve p for Polynomial of F Real;reserve f for Polynomial of F Real;
theorem :: POLYDIFFA:17
n = len f implies len (D (f,n)) = 0;
theorem :: POLYDIFFA:18
for f be Polynomial of F Real holds D (f,len f) = 0 .F Real;
theorem :: POLYDIFFA:19
n = len f −1 implies len (D (f,n)) = 1;
theorem :: POLYDIFFA:20
n = len f −1 implies D (f,n) = <% In(n!,F Real)∗f.n %>;theorem :: POLYDIFFA:21
for p being constant Polynomial of F Real holds D (p,1) = 0 .F Real;
theorem :: POLYDIFFA:22
for p being constant Polynomial of F Real holds D (p,1) = 0 .F Real;reserve a for Element of F Real;
theorem :: POLYDIFFA:23
for i be Nat, p be Polynomial of F Realholds ((a|F Real)∗’p).i = a∗p.i;
theorem :: POLYDIFFA:24
for f,g being Polynomial of F Real for a be Element of F Realst f = a|F Real holds D1(f∗’g) = (a|F Real)∗’(D1(g));
theorem :: POLYDIFFA:25
for f being Polynomial of F Real for a be Element of F Realst f = anpoly(a,0) holds D1(f) = 0 .F Real;
theorem :: POLYDIFFA:26
for f being Polynomial of F Real for a be Element of F Realst f = anpoly(a,1) holds D1(f) = anpoly(a,0);
reserve f,g for Polynomial of F Real;
theorem :: POLYDIFFA:27
for f,g st f = anpoly(1.F Real,1) holds
for i be Element of NAT holds (f∗’g).(i+1) = g.i &(f∗’g).0 = 0.F Real;
theorem :: POLYDIFFA:28
for f,g st f = anpoly(1.F Real,1) holds
D1(f∗’g) = (D1(f))∗’g + f∗’(D1(g));
theorem :: POLYDIFFA:29
for p, q be Polynomial of F Realst p is constant holds D1(p∗’q) = (D1(p))∗’q + p∗’(D1(q));

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

10/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

theorem :: POLYDIFFA:30
for x,y be Polynomial of F Real st x is non constantholds D1(x∗’y) = (D1(x))∗’y + x∗’(D1(y));
theorem :: POLYDIFFA:31
D1(f∗’g) = (D1(f))∗’g + f∗’(D1(g));
theorem :: POLYDIFFA:32
for n,f holds D1(In(n,F Real)∗f) = In(n,F Real)∗D1(f);theorem :: POLYDIFFA:33
for f be Polynomial of F Real holds
D1(f‘ˆ(m+1)) = In(m+1,F Real)∗(f‘ˆm)∗’D1(f);reserve f for non constant Polynomial of F Real;reserve a for Element of F Real;::::::::::::::::::::::::::::::::::::::::::::::::::::::: F + F’+F”+ ....Fˆ(n) − D(F + F’+F”+ ....Fˆ(n)) = F::::::::::::::::::::::::::::::::::::::::::::::::::::::reserve f for non constant Element of the carrier of Polynom−Ring F Real;::L−polynomial−membereddeﬁnition
let f be Polynomial of F Real;func HWZ(f) −> FinSequence of the carrier of Polynom−Ring F Real means:: POLYDIFFA:def 5
len it = len f & for i be Nat st i in dom it holds
it.i = ˆ(D (f,i −’ 1));end;
deﬁnition
let f be Polynomial of F Real;func HWZ2(f) −> FinSequence of the carrier of Polynom−Ring F Real means:: POLYDIFFA:def 6
len it = len f & for i be Nat st i in dom it holds
it.i = ˆ(D (f,i));end;
deﬁnition
let S be FinSequence of the carrier of Polynom−Ring F Real;func D1(S) −> FinSequence of Polynom−Ring F Real means:: POLYDIFFA:def 7
len it = len S & for i be Nat st i in dom it holds
it.i = ˆD1(˜(S/.i));end;theorem :: POLYDIFFA:34
for S be FinSequence of the carrier of Polynom−Ring F Real,v be Element of the carrier of Polynom−Ring F Real holds
D1(Sˆ<∗v∗>) = (D1(S))ˆ<∗ˆD1(˜v)∗>;theorem :: POLYDIFFA:35
for S be FinSequence of the carrier of Polynom−Ring F Real holds
D1(˜(Sum S)) = ˜Sum( D1(S));
theorem :: POLYDIFFA:36(HWZ(f)).(len f) = <% In((deg f)!,F Real)∗f.(deg f) %> &poly diﬀ(˜((HWZ(f))/.(len f))) = 0 .F Real;
theorem :: POLYDIFFA:37
for f be non constant Polynomial of F Real holds
HWZ(f) = <∗ˆf∗>ˆDel((HWZ2(f)),len f);theorem :: POLYDIFFA:38

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

11/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

D1(HWZ(f)) = HWZ2(f);theorem :: POLYDIFFA:39
for f be non constant Polynomial of F Real holds
˜Sum(HWZ(f)) = D1(˜Sum(HWZ(f))) + f;
reserve x,y for Element of the carrier of Polynom−Ring F Real;deﬁnition
let n;
let x,y be Element of the carrier of Polynom−Ring F Real;func LBZ(n,x,y) −> FinSequence of the carrier of Polynom−Ring F Realmeans:: POLYDIFFA:def 8
len it = n+1 & for i st i in dom it holds
it.i = ˆ(In(n choose (i−’1),F Real)∗((D (˜x,n+1−’i))∗’(D (˜y,i −’ 1))));
end;
theorem :: POLYDIFFA:40
LBZ(0,x,y) = <∗ x∗y ∗>;theorem :: POLYDIFFA:41
LBZ(1,x,y) = <∗ y∗ (ˆD1(˜x)), x∗ (ˆD1(˜y)) ∗>;deﬁnition
let m;
let x,y be Element of Polynom−Ring F Real;func LBZ0(m,x,y) −> FinSequence of the carrier of Polynom−Ring F Realmeans:: POLYDIFFA:def 9
len it = m & for i st i in dom it holds
it.i =ˆ(In((m choose (i−’1))+(m choose i),F Real)∗((D (˜x,m+1 −’i))∗’(D (˜y,i))));
end;
deﬁnition
let m;
let x,y be Element of the carrier of Polynom−Ring F Real;func LBZ1(m,x,y) −> FinSequence of the carrier of Polynom−Ring F Realmeans:: POLYDIFFA:def 10
len it = m &for i st i in dom it holds
it.i = ˆ(In(m choose (i−’1),F Real)∗((D (˜x,m+1 −’i))∗’(D (˜y,i))));
end;
deﬁnition
let m;
let x,y be Element of the carrier of Polynom−Ring F Real;func LBZ2(m,x,y) −> FinSequence of the carrier of Polynom−Ring F Realmeans:: POLYDIFFA:def 11
len it = m &for i st i in dom it holds
it.i = ˆ(In(m choose i,F Real)∗((D (˜x,m +1 −’i))∗’(D (˜y,i))));
end;
reserve p1,q1 for FinSequence of the carrier of Polynom−Ring F Real;
theorem :: POLYDIFFA:42
LBZ0(m,x,y) = LBZ1(m,x,y) + LBZ2(m,x,y);theorem :: POLYDIFFA:43
Sum LBZ0(n,x,y) = Sum LBZ1(n,x,y) + Sum LBZ2(n,x,y);theorem :: POLYDIFFA:44

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

12/13

Mechanized Mathematics and Its Applications, Works in Progress

Derivation of Commutative Ring (Watase Y.)

D1(LBZ0(n,x,y)) = Del(LBZ2(n+1,x,y),n+1) + Del(LBZ1(n+1,x,y),1);
theorem :: POLYDIFFA:45
Sum(D1(LBZ0(n,x,y))) =− (LBZ1(n+1,x,y)/.1) + Sum LBZ0(n+1,x,y) − (LBZ2(n+1,x,y)/.(n+1));
theorem :: POLYDIFFA:46
LBZ(n+1,x,y) = <∗ˆ((D (˜x,n+1))∗’˜y)∗>ˆ(LBZ0(n,x,y))ˆ<∗ˆ(˜x∗’(D (˜y,n+1)))∗>;
theorem :: POLYDIFFA:47
Sum(<∗ ˆ((D (˜x,n+1))∗’˜y) ∗>ˆ(LBZ0(n,x,y))ˆ<∗ ˆ(˜x∗’(D (˜y,n+1))) ∗>)= ˆ((D (˜x,n+1))∗’˜y) + Sum(LBZ0(n,x,y))+ ˆ(˜x∗’(D (˜y,n+1)));

MMA-WiP (2021), vol.3, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.3 - ISSN 2434-5458 (Online)

13/13