ホーム
おまかせ表示
ログイン
設定
寄付
ウィキブックスについて
免責事項
検索
Mizar/定義型/defpred
言語
ウォッチリストに追加
編集
<
Mizar
|
定義型
defpred P[Nat] means $1*($1-1);
P[n]≡n*(n-1);