2026-06-03 23:05
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
feat(LinearAlgebra/AffineSpace/AffineSubspace): using `AffineSubspace.direction` to reinterpret `AffineSubspace` as `Submodule` (#38731) …
Added AffineSubspace.direction_eq_self_iff_zero_mem