X := the explicit inverse formula of 2 by 2 matrix

Stream: Is there code for X?

[Junseong O]

.

[Notification Bot]

This topic was moved here from #Is there code for X? > X := the explicit inverse formula of 2 by 2 matrix? by Junseong O.

[Ruben Van de Velde]

What have you tried?

[Junseong O]

I just want to know if this theorem is registered in mathlib. It is a very famous theorem and likely to be there, but it seems that the version with explicit values for each component doesn't appear.

[Ruben Van de Velde]

Have you tried stating the theorem you're looking for?