My formalization project
0.1 Introduction
\(M,N\) を AddCommGroup とし, \(f\) を \(M\) から \(N\) への写像とする \(f\) の polar とは
\[ f(x+y) - f(x) - f(y) \]
のことを言う.
以下の等式が成り立つ.
\[ f(x + y) = f(x) + f(y) + \mathrm{Polar} f(x,y) \]
Proof
定義から明らか.
\(f,g\) を \(M\) から \(N\) への写像とする.
\[ \mathrm{Polar}(f + g) x y = \mathrm{Polar} f x y + \mathrm{Polar} g x y \]
が成り立つ.
Proof
定義より明らか.