Mathematics in Lean4 もいよいよ第6章まできました。「6.1 構造の定義」は今までの知識があればとても簡単に読み進むことができました。いわゆるレコード型のような構造およびそのレコード型に付随する関数（演算）、そしてレコード型の各フィールドあるい…