Commit 2025-12-12 02:01 5085b890

View on Github →

chore: deprecate removed modules (#32762)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/GeneralLinearGroup.lean

Created Mathlib/LinearAlgebra/Matrix/LDL.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Propose.lean

Created Mathlib/Topology/Covering.lean