Theorem LinearIndependent.of_subsingleton'

feat: add an element to a linear indep family, more general version (#31515)