Mathematics in Lean4を読んでいます。第7章1節で環の定義のあたりを勉強しています。前回は半群、モノイド、群などを定義し、また環の定義に備えて、乗法モノイドの性質を加法群に自動変換する方法なども説明しました。 ここまでくれば環を定義することがで…