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