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

@[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.symm (RingEquiv.piFinTwo R)) a i = (piFinTwoEquiv R).invFun a i

@[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

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 = let __src := piFinTwoEquiv R; { toEquiv := { toFun := ⇑(piFinTwoEquiv R), invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯, map_add' := ⋯ }