Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Eric Wieser

! This file was ported from Lean 3 source module algebra.star.prod
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Star.Basic
import Mathlib.Algebra.Ring.Prod
import Mathlib.Algebra.Module.Prod

/-!
# `Star` on product types

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

universe u v w

variable {R: Type uR : Type u: Type (u+1)Type u} {S: Type vS : Type v: Type (v+1)Type v}

namespace Prod

instance: {R : Type u} → {S : Type v} → [inst : Star R] → [inst : Star S] → Star (R × S)instance [Star: Type ?u.10 → Type ?u.10Star R: Type uR] [Star: Type ?u.13 → Type ?u.13Star S: Type vS] : Star: Type ?u.16 → Type ?u.16Star (R: Type uR × S: Type vS) where star x: ?m.26x := (star: {R : Type ?u.34} → [self : Star R] → R → Rstar x: ?m.26x.1: {α : Type ?u.43} → {β : Type ?u.42} → α × β → α1, star: {R : Type ?u.50} → [self : Star R] → R → Rstar x: ?m.26x.2: {α : Type ?u.59} → {β : Type ?u.58} → α × β → β2)

@[simp]
theorem fst_star: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).fst = star x.fstfst_star [Star: Type ?u.217 → Type ?u.217Star R: Type uR] [Star: Type ?u.220 → Type ?u.220Star S: Type vS] (x: R × Sx : R: Type uR × S: Type vS) : (star: {R : Type ?u.228} → [self : Star R] → R → Rstar x: R × Sx).1: {α : Type ?u.254} → {β : Type ?u.253} → α × β → α1 = star: {R : Type ?u.257} → [self : Star R] → R → Rstar x: R × Sx.1: {α : Type ?u.261} → {β : Type ?u.260} → α × β → α1 :=
rfl: ∀ {α : Sort ?u.271} {a : α}, a = arfl
#align prod.fst_star Prod.fst_star: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).fst = star x.fstProd.fst_star

@[simp]
theorem snd_star: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).snd = star x.sndsnd_star [Star: Type ?u.302 → Type ?u.302Star R: Type uR] [Star: Type ?u.305 → Type ?u.305Star S: Type vS] (x: R × Sx : R: Type uR × S: Type vS) : (star: {R : Type ?u.313} → [self : Star R] → R → Rstar x: R × Sx).2: {α : Type ?u.339} → {β : Type ?u.338} → α × β → β2 = star: {R : Type ?u.342} → [self : Star R] → R → Rstar x: R × Sx.2: {α : Type ?u.346} → {β : Type ?u.345} → α × β → β2 :=
rfl: ∀ {α : Sort ?u.356} {a : α}, a = arfl
#align prod.snd_star Prod.snd_star: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).snd = star x.sndProd.snd_star

theorem star_def: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), star x = (star x.fst, star x.snd)star_def [Star: Type ?u.387 → Type ?u.387Star R: Type uR] [Star: Type ?u.390 → Type ?u.390Star S: Type vS] (x: R × Sx : R: Type uR × S: Type vS) : star: {R : Type ?u.398} → [self : Star R] → R → Rstar x: R × Sx = (star: {R : Type ?u.427} → [self : Star R] → R → Rstar x: R × Sx.1: {α : Type ?u.438} → {β : Type ?u.437} → α × β → α1, star: {R : Type ?u.443} → [self : Star R] → R → Rstar x: R × Sx.2: {α : Type ?u.454} → {β : Type ?u.453} → α × β → β2) :=
rfl: ∀ {α : Sort ?u.464} {a : α}, a = arfl
#align prod.star_def Prod.star_def: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), star x = (star x.fst, star x.snd)Prod.star_def

instance: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] [inst_2 : TrivialStar R] [inst_3 : TrivialStar S],
TrivialStar (R × S)instance [Star: Type ?u.480 → Type ?u.480Star R: Type uR] [Star: Type ?u.483 → Type ?u.483Star S: Type vS] [TrivialStar: (R : Type ?u.486) → [inst : Star R] → PropTrivialStar R: Type uR] [TrivialStar: (R : Type ?u.494) → [inst : Star R] → PropTrivialStar S: Type vS] : TrivialStar: (R : Type ?u.502) → [inst : Star R] → PropTrivialStar (R: Type uR × S: Type vS)
where star_trivial _: ?m.545_ := Prod.ext: ∀ {α : Type ?u.547} {β : Type ?u.548} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = qProd.ext (star_trivial: ∀ {R : Type ?u.558} [inst : Star R] [self : TrivialStar R] (r : R), star r = rstar_trivial _: ?m.559_) (star_trivial: ∀ {R : Type ?u.586} [inst : Star R] [self : TrivialStar R] (r : R), star r = rstar_trivial _: ?m.587_)

instance: {R : Type u} → {S : Type v} → [inst : InvolutiveStar R] → [inst : InvolutiveStar S] → InvolutiveStar (R × S)instance [InvolutiveStar: Type ?u.667 → Type ?u.667InvolutiveStar R: Type uR] [InvolutiveStar: Type ?u.670 → Type ?u.670InvolutiveStar S: Type vS] : InvolutiveStar: Type ?u.673 → Type ?u.673InvolutiveStar (R: Type uR × S: Type vS)
where star_involutive _: ?m.713_ := Prod.ext: ∀ {α : Type ?u.715} {β : Type ?u.716} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = qProd.ext (star_star: ∀ {R : Type ?u.726} [inst : InvolutiveStar R] (r : R), star (star r) = rstar_star _: ?m.727_) (star_star: ∀ {R : Type ?u.749} [inst : InvolutiveStar R] (r : R), star (star r) = rstar_star _: ?m.750_)

instance: {R : Type u} →
{S : Type v} →
[inst : Semigroup R] →
[inst_1 : Semigroup S] → [inst_2 : StarSemigroup R] → [inst_3 : StarSemigroup S] → StarSemigroup (R × S)instance [Semigroup: Type ?u.847 → Type ?u.847Semigroup R: Type uR] [Semigroup: Type ?u.850 → Type ?u.850Semigroup S: Type vS] [StarSemigroup: (R : Type ?u.853) → [inst : Semigroup R] → Type ?u.853StarSemigroup R: Type uR] [StarSemigroup: (R : Type ?u.865) → [inst : Semigroup R] → Type ?u.865StarSemigroup S: Type vS] : StarSemigroup: (R : Type ?u.877) → [inst : Semigroup R] → Type ?u.877StarSemigroup (R: Type uR × S: Type vS)
where star_mul _: ?m.1967_ _: ?m.1970_ := Prod.ext: ∀ {α : Type ?u.1972} {β : Type ?u.1973} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = qProd.ext (star_mul: ∀ {R : Type ?u.1983} [inst : Semigroup R] [self : StarSemigroup R] (r s : R), star (r * s) = star s * star rstar_mul _: ?m.1984_ _: ?m.1984_) (star_mul: ∀ {R : Type ?u.2036} [inst : Semigroup R] [self : StarSemigroup R] (r s : R), star (r * s) = star s * star rstar_mul _: ?m.2037_ _: ?m.2037_)

instance: {R : Type u} →
{S : Type v} →
where star_add _: ?m.2343_ _: ?m.2346_ := Prod.ext: ∀ {α : Type ?u.2348} {β : Type ?u.2349} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = qProd.ext (star_add: ∀ {R : Type ?u.2359} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star sstar_add _: ?m.2360_ _: ?m.2360_) (star_add: ∀ {R : Type ?u.2420} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star sstar_add _: ?m.2421_ _: ?m.2421_)

instance: {R : Type u} →
{S : Type v} →
[inst : NonUnitalSemiring R] →
[inst_1 : NonUnitalSemiring S] → [inst_2 : StarRing R] → [inst_3 : StarRing S] → StarRing (R × S)instance [NonUnitalSemiring: Type ?u.2593 → Type ?u.2593NonUnitalSemiring R: Type uR] [NonUnitalSemiring: Type ?u.2596 → Type ?u.2596NonUnitalSemiring S: Type vS] [StarRing: (R : Type ?u.2599) → [inst : NonUnitalSemiring R] → Type ?u.2599StarRing R: Type uR] [StarRing: (R : Type ?u.2609) → [inst : NonUnitalSemiring R] → Type ?u.2609StarRing S: Type vS] : StarRing: (R : Type ?u.2619) → [inst : NonUnitalSemiring R] → Type ?u.2619StarRing (R: Type uR × S: Type vS) :=
{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757{ inferInstanceAs: (α : Sort ?u.2652) → [i : α] → αinferInstanceAs{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757 (StarAddMonoid: (R : Type ?u.2653) → [inst : AddMonoid R] → Type ?u.2653StarAddMonoid{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757 (R: Type uR{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757 × S: Type vS{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757)),
inferInstanceAs: (α : Sort ?u.3651) → [i : α] → αinferInstanceAs{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757 (StarSemigroup: (R : Type ?u.3652) → [inst : Semigroup R] → Type ?u.3652StarSemigroup{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757 (R: Type uR{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757 × S: Type vS{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757)) { inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757with{ inferInstanceAs (StarAddMonoid (R × S)),
inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757 }

instance: ∀ {R : Type u} {S : Type v} {α : Type w} [inst : SMul α R] [inst_1 : SMul α S] [inst_2 : Star α] [inst_3 : Star R]
[inst_4 : Star S] [inst_5 : StarModule α R] [inst_6 : StarModule α S], StarModule α (R × S)instance {α: Type wα : Type w: Type (w+1)Type w} [SMul: Type ?u.4779 → Type ?u.4778 → Type (max?u.4779?u.4778)SMul α: Type wα R: Type uR] [SMul: Type ?u.4783 → Type ?u.4782 → Type (max?u.4783?u.4782)SMul α: Type wα S: Type vS] [Star: Type ?u.4786 → Type ?u.4786Star α: Type wα] [Star: Type ?u.4789 → Type ?u.4789Star R: Type uR] [Star: Type ?u.4792 → Type ?u.4792Star S: Type vS]
[StarModule: (R : Type ?u.4796) → (A : Type ?u.4795) → [inst : Star R] → [inst : Star A] → [inst : SMul R A] → PropStarModule α: Type wα R: Type uR] [StarModule: (R : Type ?u.4821) → (A : Type ?u.4820) → [inst : Star R] → [inst : Star A] → [inst : SMul R A] → PropStarModule α: Type wα S: Type vS] : StarModule: (R : Type ?u.4844) → (A : Type ?u.4843) → [inst : Star R] → [inst : Star A] → [inst : SMul R A] → PropStarModule α: Type wα (R: Type uR × S: Type vS)
where star_smul _: ?m.4964_ _: ?m.4967_ := Prod.ext: ∀ {α : Type ?u.4969} {β : Type ?u.4970} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = qProd.ext (star_smul: ∀ {R : Type ?u.4981} {A : Type ?u.4980} [inst : Star R] [inst_1 : Star A] [inst_2 : SMul R A] [self : StarModule R A]
(r : R) (a : A), star (r • a) = star r • star astar_smul _: ?m.4982_ _: ?m.4983_) (star_smul: ∀ {R : Type ?u.5088} {A : Type ?u.5087} [inst : Star R] [inst_1 : Star A] [inst_2 : SMul R A] [self : StarModule R A]
(r : R) (a : A), star (r • a) = star r • star astar_smul _: ?m.5089_ _: ?m.5090_)

end Prod

--Porting note: removing @[simp], `simp` simplifies LHS
theorem Units.embed_product_star: ∀ [inst : Monoid R] [inst_1 : StarSemigroup R] (u : Rˣ), ↑(embedProduct R) (star u) = star (↑(embedProduct R) u)Units.embed_product_star [Monoid: Type ?u.5284 → Type ?u.5284Monoid R: Type uR] [StarSemigroup: (R : Type ?u.5287) → [inst : Semigroup R] → Type ?u.5287StarSemigroup R: Type uR] (u: Rˣu : R: Type uRˣ) :
Units.embedProduct: (α : Type ?u.5618) → [inst : Monoid α] → αˣ →* α × αᵐᵒᵖUnits.embedProduct R: Type uR (star: {R : Type ?u.6176} → [self : Star R] → R → Rstar u: Rˣu) = star: {R : Type ?u.6763} → [self : Star R] → R → Rstar (Units.embedProduct: (α : Type ?u.6766) → [inst : Monoid α] → αˣ →* α × αᵐᵒᵖUnits.embedProduct R: Type uR u: Rˣu) :=
rfl: ∀ {α : Sort ?u.7794} {a : α}, a = arfl
#align units.embed_product_star Units.embed_product_star: ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarSemigroup R] (u : Rˣ),
↑(Units.embedProduct R) (star u) = star (↑(Units.embedProduct R) u)Units.embed_product_star
```