Documentation

Mathlib.Algebra.Star.Prod

Star on product types #

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

instance Prod.instStar {R : Type u} {S : Type v} [Star R] [Star S] :
Star (R × S)
Equations
  • Prod.instStar = { star := fun (x : R × S) => (star x.1, star x.2) }
@[simp]
theorem Prod.fst_star {R : Type u} {S : Type v} [Star R] [Star S] (x : R × S) :
(star x).1 = star x.1
@[simp]
theorem Prod.snd_star {R : Type u} {S : Type v} [Star R] [Star S] (x : R × S) :
(star x).2 = star x.2
theorem Prod.star_def {R : Type u} {S : Type v} [Star R] [Star S] (x : R × S) :
star x = (star x.1, star x.2)
instance Prod.instTrivialStar {R : Type u} {S : Type v} [Star R] [Star S] [TrivialStar R] [TrivialStar S] :
Equations
  • =
Equations
instance Prod.instStarMul {R : Type u} {S : Type v} [Mul R] [Mul S] [StarMul R] [StarMul S] :
StarMul (R × S)
Equations
Equations
Equations
instance Prod.instStarModule {R : Type u} {S : Type v} {α : Type w} [SMul α R] [SMul α S] [Star α] [Star R] [Star S] [StarModule α R] [StarModule α S] :
StarModule α (R × S)
Equations
  • =