Commit 2026-02-13 13:12 ecba5414

View on Github →

chore: deprecate aliases of Classical lemmas (#34625) These are reexported in Init.Classical "for Mathlib compat".

Estimated changes

Modified Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

Modified Mathlib/Logic/Basic.lean

deleted theorem and_or_imp

modified theorem imp_and_neg_imp_iff

deleted theorem imp_iff_right_iff

deleted theorem not_imp