Commit 2022-01-11 13:55 b8d2affd
View on Github →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.