mathematics_in_lean_source
mathematics_in_lean_source copied to clipboard
avigad
Source code for the Mathematics in Lean tutorial.
In some examples the `@` symbol is used before names of theorems / functions, but it was not explained that it displays the implicit arguments. Maybe worth mentioning.
Some theorems used in the tutorial are no longer present in the current version of mathlib, e.g., `factors_count_pow`. But maybe it is not a serious problem -- I was just...
These are notes I wrote to myself during the meeting: - Describe the tactics `suggest` and `hint` - Talk about ctrl+space for better tab completion - `show_term` - `specialize`
Copy-pasting from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/MIL.20comments to make sure we don't forget 2.2: In the example at the end if one "feels cocky": Normally I would prove mul_right_inv before proving mul_one. Maybe this...
There is an example of the `choose` tactic commented out in the chapter _Sets, Functions, and Relations_. We should decide whether to discuss it there or wait until a later...
From Zulip: > Another general remark about my tutorials: I never tell my students about simp. That would be too powerful, and it would encourage them to try simp every...
We need to explain the `finset` vs `fintype` vs `finite` mess somewhere, probably in Chapter 4.
Not an actual issue up to now, but let's record that we should carefully monitor https://github.com/leanprover-community/mathlib/pull/3083