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

Merged

Commits

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

kckennylau committed 6 years ago
feat(linear_algebra/basis): generalize independence of characters to integral domains

kckennylau committed 6 years ago
chore(linear_algebra/basis): change proofs

kckennylau committed 6 years ago
Merge branch 'master' into dedekind-indep

mergify[bot] committed 6 years ago
commenting the proof

kim-em committed 6 years ago
Merge branch 'dedekind-indep' of github.com:leanprover-community/mathlib into dedekind-indep

kim-em committed 6 years ago