Theorems · Definition · ring theory

RingEquiv.piFinTwo

(R : Fin 2 → Type u_1) → [inst : (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.

Defined in

Mathlib.Algebra.Ring.Fin

Cited by

2 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound

Assumes

Semiring