Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-16 17:03 42f7ca0f

View on Github →

chore(linear_algebra/linear_independent): use is_empty ι instead of ¬nonempty ι (#8331)

Estimated changes

Modified src/field_theory/fixed.lean

Modified src/linear_algebra/linear_independent.lean

modified theorem linear_independent_empty_type

Modified src/ring_theory/polynomial/bernstein.lean