Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-18 22:27 0bcfff99

View on Github →

feat(linear_algebra/basis) remove several [nontrivial R] (#7642) We remove some unnecessary nontrivial R.

Estimated changes

Modified src/linear_algebra/basis.lean

modified def basis.reindex_range

modified theorem basis.reindex_range_apply

modified theorem basis.reindex_range_repr'

modified theorem basis.reindex_range_repr

modified theorem basis.reindex_range_repr_self

modified theorem basis.reindex_range_self

Modified src/linear_algebra/finsupp.lean

added def module.subsingleton_equiv

Modified src/linear_algebra/matrix/to_lin.lean

modified theorem linear_map.to_matrix_alg_equiv_reindex_range

modified theorem linear_map.to_matrix_reindex_range