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