BitVec lemmas

Stream: mathlib4

[Jakob von Raumer]

I agree with the sentiment behind keeping the lemmas about BitVec in mathlib at a minimum, but shouldn't we at least have the ring iso to ZMod (2 ^ m) in there as an off-bridge? Right now it seems it's a CommRing instance without any algebraic properties proven about it? /cc @Kim Morrison @Alex Keizer @Patrick Massot

[Eric Wieser]

That equivalence is not true when m=0

[Eric Wieser]

I'd expect the iso with Fin (2^m) though

[Eric Wieser]

If you want Zmod then I'd expect you to have to compose with another iso

[Jakob von Raumer]

Shouldn't all algebraic statements rather be about ZMod? I thought the ring structure on Fin is more or less only defined to then put it on ZMod

[Jakob von Raumer]

Hm, though I guess both have their applications in terms of what the zero case should be

[Eric Wieser]

The nice thing about the Fin spelling is that the simplification lemmas can reduce the iso to ofFin and toFin, without needing to introduce new ofZMod and toZMod

[Patrick Massot]

I have no opinion about BitVec except I know that having BitVec stuff in Mathlib is annoying to the FRO.

[Eric Wieser]

Given we have the Ring instance in mathlib, I think a PR to add the corresponding RingEquiv alongside it would be very reasonable

[Jakob von Raumer]

Will do!

[Jakob von Raumer]

#20322