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