jurupapa https://blog.hatena.ne.jp/jurupapa/ Maxima で綴る数学の旅 https://maxima.hatenablog.jp/ 数学 Mathematics in Lean4を読んでいます。第7章1節で環の定義のあたりを勉強しています。前回は半群、モノイド、群などを定義し、また環の定義に備えて、乗法モノイドの性質を加法群に自動変換する方法なども説明しました。 ここまでくれば環を定義することができます。 class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where /-- Multiplication is left distributive over addition -/ left_distrib : ∀ a b c : R, a *… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmaxima.hatenablog.jp%2Fentry%2F2024%2F11%2F06%2F231010" title="-数学- Lean4のお勉強　環を定義する - Maxima で綴る数学の旅" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> https://cdn-ak.f.st-hatena.com/images/fotolife/j/jurupapa/20241004/20241004131829.jpg Hatena Blog https://hatena.blog 2024-11-06 23:10:10 rich https://maxima.hatenablog.jp/entry/2024/11/06/231010 1.0 100%