Commit 2023-01-31 07:39 d3b170e4

View on Github →

Chore: drop _root_.not_not, export it from Classical (#1954) This way we don't get a name clash when we open Classical.

Estimated changes

Modified Mathlib/Control/Fix.lean

Modified Mathlib/Logic/Basic.lean

deleted theorem not_not

Modified Mathlib/Logic/Nontrivial.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Modified Mathlib/Order/Filter/Ultrafilter.lean