|
|
|
|
|
|
by kmill
2032 days ago
|
|
|
Correcting my non-expert inaccuracies in this thread: I just learned that Diaconescu's theorem depends on the axiom of choice, which I'd missed even though I'd glanced at the code for classical.em a few times. So, LEM definitely depends on the axiom of choice in Lean. |
|
|