Update on the Lean formalization: it does compile! Now it is somewhat difficult to check the definitions, as they are spread out over many files and declarations. In particular for the definition of the Ricci tensor of a left-invariant metric (both given as 6×6-matrices) one has to carefully […]
mathstodon.xyz
Original post on mathstodon.xyz