Commit 2025-08-22 23:56 5b472055

View on Github →

chore(LinearAlgebra/AffineSpace/AffineSubspace): deprecate mem_mk'_iff_vsub_mem (duplicate) (#28519)

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean

Modified Mathlib/Geometry/Euclidean/Sphere/Tangent.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

modified theorem AffineSubspace.mem_mk'

deleted theorem AffineSubspace.mem_mk'_iff_vsub_mem