今回は参考文献から離れて、群論の形式化を楽しみましょう。
【動画１２－０１】、【動画１２－０２】、【動画１２－０３】を参考にして、下の画像【演習１２－０１】、【演習１２－０２】、【演習１２－０３】と同じ入力をしてみましょう。
それではここでレポート課題を提示します。
回答をLEAN Web Editor上で作成したら、
テキストエディタにコピー＆ペーストして、
文字コード UTF-8 の txt形式で保存して下さい。
そのtxtファイルをMoodleを通じて提出して下さい。
他の文字コードを使うと \forall などが消えてしまう恐れがあります。注意して下さい。
課題の内容と締め切りは下をご覧下さい。
ブラウザからPDFファイルを作成する方法は
https://shop-pro.jp/manual/browser_pdf
などが参考になります。
Moodleのコースコードは
2020-W20102001
です。
課題：自然数 1 のみからなる集合 {1}と、自然数の積 * のペア( {1}, * )が群になることを示しなさい。
ヒント：１つだけの元からなる集合は singleton と呼ばれます。
要素を扱う関数として data.set などに 文字列mem_singltonを含む関数や、文字列singletonを含む関数が便利です。また、LEANの補間機能などを活用して、必要な関数を探してみましょう。
signletonまわりの関数を調べることで、１元からなる集合の記法がわかります。そこから、１元からなる集合を定義する書き方もわかります。
締切：６月１９日（金）１７：００
