<h1 id="%E3%81%93%E3%81%AE%E8%A8%98%E4%BA%8B%E3%81%AB%E3%81%A4%E3%81%84%E3%81%A6" data-line="0" class="code-line">
<a class="header-anchor-link" href="#%E3%81%93%E3%81%AE%E8%A8%98%E4%BA%8B%E3%81%AB%E3%81%A4%E3%81%84%E3%81%A6" aria-hidden="true"></a> この記事について</h1>
<p data-line="1" class="code-line">以下のヨビノリ群論入門の流れに沿ってLean4で群論を形式化していきます。</p>
<p data-line="3" class="code-line"><span class="embed-block zenn-embedded zenn-embedded-card"><iframe id="zenn-embedded__e110164cac754" src="https://embed.zenn.studio/card#zenn-embedded__e110164cac754" data-content="https%3A%2F%2Fyoutube.com%2Fplaylist%3Flist%3DPLDJfzGjtVLHn9XEfkMHH157Q-IgLiI8p9%26si%3DhmdWqnOu631SbBSb" frameborder="0" scrolling="no" loading="lazy"></iframe></span><a href="https://youtube.com/playlist?list=PLDJfzGjtVLHn9XEfkMHH157Q-IgLiI8p9&amp;si=hmdWqnOu631SbBSb" style="display:none" target="_blank" rel="nofollow noopener noreferrer">https://youtube.com/playlist?list=PLDJfzGjtVLHn9XEfkMHH157Q-IgLiI8p9&amp;si=hmdWqnOu631SbBSb</a></p>
<p data-line="5" class="code-line">実数の性質などの具体例の部分を除いて、なるべくMathlibで用意された定義や定理を使わないことを目指しています。</p>
<h1 id="%E7%9B%AE%E6%AC%A1" data-line="7" class="code-line">
<a class="header-anchor-link" href="#%E7%9B%AE%E6%AC%A1" aria-hidden="true"></a> 目次</h1>
<p data-line="8" class="code-line"><a href="https://zenn.dev/tanaka0000/articles/56956b5f576bed" target="_blank">ヨビノリ群論入門②をLean4で形式化</a></p>
<p data-line="10" class="code-line"><a href="https://zenn.dev/tanaka0000/articles/7aa64e9f806491" target="_blank">Lean4で全単射や逆関数の性質を証明</a></p>
<p data-line="12" class="code-line"><a href="https://zenn.dev/tanaka0000/articles/72bd14ff724b4a" target="_blank">ヨビノリ群論入門③をLean4で形式化</a></p>


ヨビノリ群論入門をLean4で形式化

この記事について

目次

Discussion