All Questions
4
questions
2
votes
1
answer
206
views
Lemma about splitting of homogeneous polynomial equations into irreducible equations
Proof assistants, and Lean, are completely new to me.
How can I derive the following simple lemma in Lean?
How can I let Lean check if the lemma is correctly written?
How can I let Lean check if the ...
- 131
9
votes
1
answer
642
views
How to define curry in Lean
I just started with Lean and with this nice SE.
In the official web book/tutorial, when explaining definitions https://leanprover.github.io/theorem_proving_in_lean/index.html they ask to complete this ...
- 193
8
votes
2
answers
533
views
Strong induction on ℕ with function α → ℕ
I have the following problem. I have a type $\alpha$, function $f : \alpha \to \mathbb{N}$ and predicate $P : \alpha \to \mathrm{Prop}$ and I want to prove that for all $a : \alpha, P a$.
How could ...
- 137
20
votes
2
answers
735
views
What is the difference between refl and rfl in Lean 3?
I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...
- 410