Commit 2024-12-01 09:59 e4876c14

View on Github →

chore: delete deprecated lemmas (#19627) This deletes a few deprecated lemmas, allowing us to clean up some imports.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Algebra/Hom.lean

Modified Mathlib/Algebra/Group/AddChar.lean

Modified Mathlib/Algebra/TrivSqZeroExt.lean

Modified Mathlib/Data/Matrix/ConjTranspose.lean

Modified Mathlib/Data/Matrix/Notation.lean

Modified Mathlib/RingTheory/Finiteness/Defs.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

Modified scripts/noshake.json