Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-10 23:30 8910f6d9

View on Github →

feat(ring_theory/discriminant): remove an assumption (#11359) We remove a nonempty assumption.

Estimated changes

Modified src/ring_theory/discriminant.lean

modified theorem algebra.discr_not_zero_of_linear_independent