THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file collects some basic results involving rings and the
Main results #
ring_equiv.fin_two: The product over
fin 2 of some rings is the cartesian product
The product over
fin 2 of some rings is just the cartesian product of these rings.