mathlib3 documentation

algebra.ring.fin

Rings and fin #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

@[simp]
theorem ring_equiv.pi_fin_two_symm_apply (R : fin 2 Type u_1) [Π (i : fin 2), semiring (R i)] (ᾰ : R 0 × R 1) (i : fin 2) :
@[simp]
theorem ring_equiv.pi_fin_two_apply (R : fin 2 Type u_1) [Π (i : fin 2), semiring (R i)] (ᾰ : Π (i : fin 2), R i) :
def ring_equiv.pi_fin_two (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