mathlib documentation

algebra.star.prod

star on product types #

We put a has_star structure on product types that operates elementwise.

@[protected, instance]
def prod.has_star {R : Type u} {S : Type v} [has_star R] [has_star S] :
has_star (R × S)
Equations
@[simp]
theorem prod.fst_star {R : Type u} {S : Type v} [has_star R] [has_star S] (x : R × S) :
@[simp]
theorem prod.snd_star {R : Type u} {S : Type v} [has_star R] [has_star S] (x : R × S) :
theorem prod.star_def {R : Type u} {S : Type v} [has_star R] [has_star S] (x : R × S) :
@[protected, instance]
def prod.star_module {R : Type u} {S : Type v} {α : Type w} [has_scalar α R] [has_scalar α S] [has_star α] [has_star R] [has_star S] [star_module α R] [star_module α S] :
star_module α (R × S)