Mathlib.Algebra.Ring.Fin

(R : Fin 2 → Type*) [∀ i, Semiring (R i)] : (∀ i : Fin 2, R i) ≃+* R 0 × R 1

Full source

/-- The product over `Fin 2` of some rings is just the cartesian product of these rings. -/
@[simps]
def RingEquiv.piFinTwo (R : Fin 2 → Type*) [∀ i, Semiring (R i)] :
    (∀ i : Fin 2, R i) ≃+* R 0 × R 1 :=
  { piFinTwoEquiv R with
    toFun := piFinTwoEquiv R
    map_add' := fun _ _ => rfl
    map_mul' := fun _ _ => rfl }

Ring equivalence between product over `Fin 2` and Cartesian product

Informal description

The ring equivalence `RingEquiv.piFinTwo` establishes a bijection between the product of rings indexed by `Fin 2` (i.e., pairs of elements where the first is from the ring `R 0` and the second is from the ring `R 1`) and the Cartesian product `R 0 × R 1`. This equivalence preserves both the additive and multiplicative ring structures.

Main results