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.

Equations

• RingEquiv.piFinTwo R = { toFun := ⇑(piFinTwoEquiv R), invFun := (piFinTwoEquiv R).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingEquiv.piFinTwo_apply (R : Fin 2 → Type u_1) [(i : Fin 2) → Semiring (R i)] (a : (i : Fin 2) → R i) : (RingEquiv.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), (RingEquiv.piFinTwo R).symm a i = (piFinTwoEquiv R).invFun a i