Commit 2020-10-05 11:38 72360845

refactor(linear_algebra/matrix): consistent naming (#4345) The naming of the maps between linear_map and matrix was a mess. This PR proposes to clean it up by standardising on two forms:

• linear_map.to_matrix and matrix.to_linear_map are the equivalences (in the respective direction) between M₁ →ₗ[R] M₂ and matrix m n R, given bases for M₁ and M₂.
• linear_map.to_matrix' and matrix.to_lin' are the equivalences between ((n → R) →ₗ[R] (m → R)) and matrix m n R in the respective directions The following declarations are renamed:
• comp_to_matrix_mul -> linear_map.to_matrix'_comp
• linear_equiv_matrix -> linear_map.to_matrix
• linear_equiv_matrix_{apply,comp,id,mul,range} -> linear_map.to_matrix_{apply,comp,id,mul,range}
• linear_equiv_matrix_symm_{apply,mul,one} -> matrix.to_lin_{apply,mul,one}
• linear_equiv_matrix' -> linear_map.to_matrix'
• linear_map.to_matrix_id ->linear_map.to_matrix'_id
• matrix.mul_to_lin -> matrix.to_lin'_mul
• matrix.to_lin -> matrix.mul_vec_lin (which should get simplified to matrix.to_lin')
• matrix.to_lin_apply -> matrix.to_lin'_apply
• matrix.to_lin_one -> matrix.to_lin'_one
• to_lin_to_matrix -> matrix.to_lin'_to_matrix'
• to_matrix_to_lin -> linear_map.to_matrix'_to_lin' The following declarations are deleted as unnecessary:
• linear_equiv_matrix_apply' (use linear_map.to_matrix_apply instead)
• linear_equiv_matrix'_apply (the original linear_map.to_matrix doesn't exist any more)
• linear_equiv_matrix'_symm_apply (the original matrix.to_lin doesn't exist any more)
• linear_map.to_matrixₗ (use linear_map.to_matrix' instead)
• linear_map.to_matrix (use linear_map.to_matrix' instead)
• linear_map.to_matrix_of_equiv (use linear_map.to_matrix'_apply instead)
• matrix.eval (use matrix.to_lin' instead)
• matrix.to_lin.is_add_monoid_hom (use linear_equiv.to_add_monoid_hom instead)
• matrix.to_lin_{add,zero,neg} (use linear_equiv.map_{add,zero,neg} matrix.to_lin' instead)
• matrix.to_lin_of_equiv (use matrix.to_lin'_apply instead) Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Refactoring.20.60linear_map.20.3C-.3E.20matrix.60