Commit 2024-09-25 00:50 9910ecab

View on Github →

chore: bump dependencies and adapt to updated namespaces (#17117)

Estimated changes

Modified Mathlib/Tactic/CategoryTheory/Elementwise.lean

Modified Mathlib/Tactic/Linter/Lint.lean

added def Batteries.Tactic.Lint.deprecatedNoSince

added def Batteries.Tactic.Lint.structureInType

deleted def Std.Tactic.Lint.deprecatedNoSince

deleted def Std.Tactic.Lint.structureInType

Modified Mathlib/Tactic/Widget/Calc.lean

Modified lake-manifest.json