Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-10 19:12 b7ac8334

View on Github →

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.

Estimated changes