Skip to content

Commit

Permalink
Update lun. 18 déc. 2023 17:25:35 EST
Browse files Browse the repository at this point in the history
  • Loading branch information
PatrickMassot committed Dec 18, 2023
1 parent 5473788 commit 823e61a
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion C02_Basics.html
Original file line number Diff line number Diff line change
Expand Up @@ -425,7 +425,7 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
characterized axiomatically, like rings.
Moreover, Lean supports <em>generic reasoning</em> about
both abstract and concrete structures,
and can be trained to recognized appropriate instances.
and can be trained to recognize appropriate instances.
So any theorem about rings can be applied to concrete rings
like the integers, <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code>, the rational numbers, <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>,
and the complex numbers <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>.
Expand Down
Binary file modified mathematics_in_lean.pdf
Binary file not shown.

0 comments on commit 823e61a

Please sign in to comment.