Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-08-21 10:55
2b074c2a
View on Github →
chore(LinearAlgebra/AffineSpace): deprecate
coe_injective
(duplicate) (
#28457
)
Estimated changes
Modified
Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
deleted
theorem
ContinuousAffineEquiv.coe_injective