mathlib3

8eaf478a - feat(linear_algebra/basis): Dedekind's linear independence of characters (#1595)

feat(linear_algebra/basis): Dedekind's linear independence of characters (#1595) * feat(linear_algebra/basis): Dedekind's linear independence of characters * feat(linear_algebra/basis): generalize independence of characters to integral domains * chore(linear_algebra/basis): change proofs * commenting the proof