star on product types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We put a has_star structure on product types that operates elementwise.
@[protected, instance]
Equations
- prod.has_star = {star := λ (x : R × S), (has_star.star x.fst, has_star.star x.snd)}
@[simp]
theorem
prod.fst_star
{R : Type u}
{S : Type v}
[has_star R]
[has_star S]
(x : R × S) :
(has_star.star x).fst = has_star.star x.fst
@[simp]
theorem
prod.snd_star
{R : Type u}
{S : Type v}
[has_star R]
[has_star S]
(x : R × S) :
(has_star.star x).snd = has_star.star x.snd
theorem
prod.star_def
{R : Type u}
{S : Type v}
[has_star R]
[has_star S]
(x : R × S) :
has_star.star x = (has_star.star x.fst, has_star.star x.snd)
@[protected, instance]
def
prod.has_trivial_star
{R : Type u}
{S : Type v}
[has_star R]
[has_star S]
[has_trivial_star R]
[has_trivial_star S] :
has_trivial_star (R × S)
@[protected, instance]
def
prod.has_involutive_star
{R : Type u}
{S : Type v}
[has_involutive_star R]
[has_involutive_star S] :
has_involutive_star (R × S)
Equations
@[protected, instance]
def
prod.star_semigroup
{R : Type u}
{S : Type v}
[semigroup R]
[semigroup S]
[star_semigroup R]
[star_semigroup S] :
star_semigroup (R × S)
@[protected, instance]
def
prod.star_add_monoid
{R : Type u}
{S : Type v}
[add_monoid R]
[add_monoid S]
[star_add_monoid R]
[star_add_monoid S] :
star_add_monoid (R × S)
@[protected, instance]
def
prod.star_ring
{R : Type u}
{S : Type v}
[non_unital_semiring R]
[non_unital_semiring S]
[star_ring R]
[star_ring S] :
Equations
@[protected, instance]
def
prod.star_module
{R : Type u}
{S : Type v}
{α : Type w}
[has_smul α R]
[has_smul α S]
[has_star α]
[has_star R]
[has_star S]
[star_module α R]
[star_module α S] :
star_module α (R × S)
@[simp]
theorem
units.embed_product_star
{R : Type u}
[monoid R]
[star_semigroup R]
(u : Rˣ) :
⇑(units.embed_product R) (has_star.star u) = has_star.star (⇑(units.embed_product R) u)