mathlib3

feat(linear_algebra/basis): Dedekind's linear independence of characters

#1595

Merged