mathlib3 documentation

algebra.star.prod

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]
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]
@[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)