mathlib
10ee5ede - chore(logic/basic): golf a proof (#17807)

Commit

3 years ago

chore(logic/basic): golf a proof (#17807) This is the way `not_or` is proved in Lean 4 Std.

Author

urkud

Parents