Commit 2024-08-16 16:22 9ab6a770

View on Github →

chore(Logic): remove bare open Classical (#15836)

Estimated changes

Modified Mathlib/Logic/Denumerable.lean

modified theorem Nat.Subtype.exists_succ

Modified Mathlib/Logic/Nontrivial/Basic.lean

Modified Mathlib/Logic/Nontrivial/Defs.lean

Modified Mathlib/Logic/Small/Basic.lean

Modified Mathlib/Logic/Small/Defs.lean