Commit 2024-09-10 17:34 0dfdf3d8

View on Github →

chore: deprecate most of Init.Logic (#16438) And bunch up the non-deprecated declarations.

Estimated changes

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/Algebra/Group/Action/Prod.lean

Modified Mathlib/Algebra/GroupWithZero/Action/Prod.lean

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

Modified Mathlib/Combinatorics/SetFamily/KruskalKatona.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/Fintype/Perm.lean

Modified Mathlib/Data/Fintype/Quotient.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Ordmap/Ordnode.lean

Modified Mathlib/Data/Ordmap/Ordset.lean

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/Init/Algebra/Classes.lean

Modified Mathlib/Init/Logic.lean

deleted theorem heq_prop

deleted theorem not_of_eq_false

Modified Mathlib/Logic/Basic.lean

modified theorem by_contradiction

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Logic/Nontrivial/Defs.lean

Modified Mathlib/Logic/Unique.lean

Modified Mathlib/NumberTheory/FermatPsp.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/SetTheory/Game/Short.lean

Modified Mathlib/Tactic/CC/Lemmas.lean

Modified test/DefEqTransformations.lean

Modified test/cases.lean

Modified test/solve_by_elim/basic.lean