Theorem LinearIndepOn.insert'

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