Theorem AffineIndependent.vectorSpan_image_eq_iff

Modification history

2025-12-05 16:31

Mathlib/LinearAlgebra/AffineSpace/Independent.lean

feat(LinearAlgebra/AffineSpace/Independent): injectivity of spans of images (#31979) …

Added AffineIndependent.vectorSpan_image_eq_iff View on Github →