mathlib

b8d2affd - 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`.