Commit 2024-11-19 09:31 01fc25a2
View on Github →chore(Algebra/Bilinear): deprecate duplicated injectivity lemmas (#19231) These are less general versions of results stated elsewhere. This partially deprecates @Vierkantor's https://github.com/leanprover-community/mathlib3/pull/6588. Also tidy the one caller of these lemmas.