Documentation

Mathlib.Algebra.Ring.Fin

Rings and Fin #

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

Main results #

@[simp]
theorem RingEquiv.piFinTwo_symm_apply (R : Fin 2Type 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
@[simp]
theorem RingEquiv.piFinTwo_apply (R : Fin 2Type u_1) [(i : Fin 2) → Semiring (R i)] (a : (i : Fin 2) → R i) :
def RingEquiv.piFinTwo (R : Fin 2Type 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
Instances For