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 #
ring_equiv.fin_two: The product overfin 2of some rings is the cartesian product
@[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) :
⇑(ring_equiv.pi_fin_two R) ᾰ = ⇑(pi_fin_two_equiv R) ᾰ
The product over fin 2 of some rings is just the cartesian product of these rings.
Equations
- ring_equiv.pi_fin_two R = {to_fun := ⇑(pi_fin_two_equiv R), inv_fun := (pi_fin_two_equiv R).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}