English
The product over Fin 2 of a family of semirings is ring-isomorphic to the Cartesian product of its two components; more precisely, there is a ring equivalence between the family (R i) and R 0 × R 1.
Русский
Произведение по Fin 2 семирингов конвертируется в декартово произведение; существует кольцевое эквивалентность между семирингами и их двумя компонентами.
LaTeX
$$$\\bigl(\\forall i: \\mathrm{Fin}(2),\\, R(i)\\bigr) \\cong_{Ring} R(0) \\times R(1)$$$
Lean4
/-- The product over `Fin 2` of some rings is just the Cartesian product of these rings. -/
@[simps]
def piFinTwo (R : Fin 2 → Type*) [∀ i, Semiring (R i)] : (∀ i : Fin 2, R i) ≃+* R 0 × R 1 :=
{ piFinTwoEquiv R with
toFun := piFinTwoEquiv R
map_add' := fun _ _ => rfl
map_mul' := fun _ _ => rfl }
