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 = Equiv.invFun ((i : Fin 2) → R i) (R 0 × R 1) (piFinTwoEquiv R) 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

• One or more equations did not get rendered due to their size.