Rings and Fin

This file collects some basic results involving rings and the Fin type

Main results

• RingEquiv.piFinTwo: The product over Fin 2 of some rings is the Cartesian product

def RingEquiv.piFinTwo (R : Fin 2 → Type u_1) [(i : Fin 2) → Semiring (R i)] : ((i : Fin 2) → R i) ≃+* R 0 × R 1

The product over Fin 2 of some rings is just the Cartesian product of these rings.

@[simp]

theorem RingEquiv.piFinTwo_apply (R : Fin 2 → Type u_1) [(i : Fin 2) → Semiring (R i)] (a : (i : Fin 2) → R i) : (piFinTwo R) a = (piFinTwoEquiv R) a

@[simp]

theorem RingEquiv.piFinTwo_symm_apply (R : Fin 2 → Type u_1) [(i : Fin 2) → Semiring (R i)] (a✝ : R 0 × R 1) (i : Fin 2) : (piFinTwo R).symm a✝ i = (piFinTwoEquiv R).invFun a✝ i