mathlib3

b7ac8334 - feat(ring_theory/discriminant): add the discriminant of a family of vectors (#10350)

feat(ring_theory/discriminant): add the discriminant of a family of vectors (#10350) We add the definition and some basic results about the discriminant. From FLT-regular. - [x] depends on: #10657 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>