Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-16 10:20 a1dda1e9

View on Github →

feat(linear_algebra/matrix): linear maps are linearly equivalent to matrices (#1310)

  • linear map to matrix (WIP)
  • WIP
  • feat (linear_algebra/matrix): lin_equiv_matrix
  • feat (linear_algebra.basic): linear_equiv.arrow_congr, std_basis_eq_single
  • change unnecessary vector_space assumption for equiv_fun_basis to module
  • add docstrings and refactor
  • add docstrings
  • move instance to pi_instances
  • add docstrings + name change
  • remove duplicate instance

Estimated changes

added def equiv_fun_basis
added theorem module.card_fintype
modified theorem vector_space.card_fintype
added def lin_equiv_matrix
added theorem to_lin_to_matrix
added theorem to_matrix_to_lin