Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-03 17:57 018309f0

View on Github →

chore(linear_algebra/basis): replace explicit arguments for 0 ≠ 1 with nontrivial R (#3678)

Estimated changes

Modified archive/sensitivity.lean

Modified src/linear_algebra/basis.lean

modified theorem eq_of_linear_independent_of_span_subtype

modified theorem is_basis.injective

modified theorem le_of_span_le_span

modified theorem linear_independent.injective

modified theorem linear_independent.ne_zero

modified theorem span_le_span_iff

modified theorem surjective_of_linear_independent_of_span

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/finite_dimensional.lean

Modified src/linear_algebra/matrix.lean

Modified src/ring_theory/noetherian.lean