Creating many representations for the same thing.

Stream: general

[Juho Kupiainen]

As an example, mathlib defines the matrix type, and a lot of class instances for it. Now, I can represent the information of a n by 1 matrix in a vector type of length n. What would be the easiest way to get all the type class instances like has_add and add_comm_group by creating a bijection?

[Kevin Buzzard]

This is a great question :-)

[Kevin Buzzard]

I think the answer is that we need a tactic to do this and it's not there.

[Yury G. Kudryashov]

Some theorems are in equiv/algebra but I'd prefer to have a tactic

[Johan Commelin]

The tactic is called transport and it has been discussed at great length, but it's seen almost no use. Partly because it's not as magical as we would like it to be.