mathematics_in_lean_source

mathematics_in_lean_source copied to clipboard

The exercise about ``` def weightedAverage {n : ℕ} (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : StandardSimplex n) : StandardSimplex n...

PatrickMassot

Present tactic unfold

1

As a beginner, I am finding tactic `unfold` very handy while I'm not able to "see through definitions" yet. Maybe it could be mentioned at some point, together with its...

giomasce

https://github.com/avigad/mathematics_in_lean_source/blob/3fa84e6b3135a3ae41edc6ca195abf0fb1ae3ac3/user_repo_source/README.md?plain=1#L43 https://github.com/leanprover/vscode-lean4/issues/444

sebeaumont

`def myGroup := PresentedGroup {.of () ^ 3} deriving Group` gives the error `invalid dotted identifier notation, expected type is not of the form (... → C ...) where C...

KunihikoK3

Names of propositions `pge` and `primep` don't match when destructing `Nat.exists_infinite_primes`

yannickseurin

Section 3.6 introduces the `convert` tactic, but does not explain the `convert ... using` syntax. It is used in the proof of `theorem convergesTo_mul` towards the end of the section....

yannickseurin

Batch of typos in Chapter 3

yannickseurin

Exercise for S2.5 requires setting implicit arguments

4

I went through exercises of Chapter 2 and they can all be solved with the information in the chapter, except for this one from Section 2.5: > example : x...

yannickseurin

Section 2.2: Definition of substraction in a general ring

2

I'm currently going through MIL and everything reads really well, but this passage in Section 2.2 made me pause and wonder: > In Lean, subtraction in a ring is provably...

yannickseurin

Solutions in C02S04/05 use `repeat'` but this tactic is not described in the text and everything works fine with `repeat`.

yannickseurin