Commit 2026-09-30 17:01 0db6cb99
View on Github →feat(LinearAlgebra/LinearIndependent/Basic): promote LinearIndepOn.id_imageₛ to iff, and add smul_set version (#43487)
This is the "id"-version of LinearMap.linearIndepOn_iff_of_injOn. Now LinearIndepOn.id_imageₛ is an alias for the mpr direction.
The smul version looks similar to LinearIndependent.group_smul_iff, but theirs needs a group action on the ring, not the module.