Noperthedron
The Noperthedron does not have Rupert Property: a proof in Lean4
Sort by
Require Order
mathlib
v4.33.1The math library of Lean 4tryAtEachStep
05ff580Try a tactic at each step in a Lean proof.checkdecls
lean4.18.0Tiny Lean library to check existence of declarations