Theorem linearIndepOn_id_smul_set_iff

Modification history

2026-09-30 17:01
Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
feat(LinearAlgebra/LinearIndependent/Basic): promote `LinearIndepOn.id_imageₛ` to iff, and add `smul_set` version (#43487) …
Added linearIndepOn_id_smul_set_iffView on Github →