refactor(ring_theory/discriminant): refactor discr_not_zero_of_linear_independent (#11370)
refactor(ring_theory/discriminant): refactor discr_not_zero_of_linear_independent (#11370)

`(hcard : fintype.card ι = finite_dimensional.finrank K L) (hli : linear_independent K b)` is better expressed as `b : basis ι K L`.





leanprover-community/mathlib,leanprover-community/mathlib