Index of sublattice is determinant

Stream: Is there code for X?

[Andrew Yang]

Do we know that for lattices $L \subseteq L'$ in $\mathbb{Q}^n$ with bases $b$ and $b'$,
$[L' : L]$ is the determinant of the matrix sending $b$ to $b'$?

[Junyan Xu]

I recall seeing something like that in the Bruhat--Tits repo
cc @Xavier Roblot @Christian Merten

[Xavier Roblot]

There is nothing directly about that in docs#ZLattice.covolume , but I think it should not be too hard to deduce from what we have since we have docs#Basis.SmithNormalForm already

[Xavier Roblot]

@Andrew Yang , I think the result you want is here #22902

[Xavier Roblot]

And the follow up: #22940