mathematics_in_lean_source
mathematics_in_lean_source copied to clipboard
avigad
Source code for the Mathematics in Lean tutorial.
The crazy parentheses in the following snippet from Chapter 5 are probably either a mathport issue of working around a precedence bug that no longer exists. ```lean example (f :...
From Jireh [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/New.20chapter.20in.20MIL/near/398351301) about the groups and rings chapter: 1. Early on when discussing morphisms, the proofs used `f.map_mul` or `f.map_inv` as opposed to `map_mul f` and `map_inv f`....
The challenge exercise at the end of section 2.3 proving `|a * b| ≤ (a ^ 2 + b ^ 2) / 2` uses the `constructor` tactic, but this tactic...
In Chapter 5, we have ``` example : fac 0 = 1 := by simp [fac] ``` which is misleading since giving `[fac]` plays no role.
#121 added a comment about structural eta reduction to Chapter 6, Section 1, without explaining it.
We should set the autoImplicit flag to false, to match mathlib. See Eric Wieser's comments at #110.
The metric space on `α × β` uses the `max`-distance, not the Euclidean distance, and maybe give a forward-reference to the Euclidean distance.
The linter currently complains about unused variables e.g. in `fun a b aleb ↦ mf (mg aleb)`. We should probably explain this somewhere and then replace unused variables by underscores.