Cardinality of SpecialLinearGroup over a finite field

Stream: Is there code for X?

[Rado Kirov]

I see https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.html#Matrix.card_GL_field

but can't seem to find the corresponding theorem for the SpecialLinearGroup.

Also, there are so many different cardinality functions Fintype.card, Nat.card, and others, which one is the canonical one to use for such theorems.

[Kenny Lau]

Nat.card doesn't use any instance so it avoids diamonds so it's "more general"

[Kevin Buzzard]

Nat.card works great for groups, because the junk answer 0 can only mean that the group is infinite, as every group has at least one element. It also makes a lot of theorems true in the infinite case e.g. "if $G\subseteq H$ then order of $G$ divides order of $H$" etc.