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.pi
! 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.Pi

/-!
# `star` on pi types

We put a `Star` structure on pi types that operates elementwise, such that it describes the
complex conjugation of vectors.
-/

universe u v w

variable {I: Type uI : Type u: Type (u+1)Type u}

-- The indexing type
variable {f: I β Type vf : I: Type uI β Type v: Type (v+1)Type v}

-- The family of types already equipped with instances
namespace Pi

instance: {I : Type u} β {f : I β Type v} β [inst : (i : I) β Star (f i)] β Star ((i : I) β f i)instance [β i: ?m.17i, Star: Type ?u.20 β Type ?u.20Star (f: I β Type vf i: ?m.17i)] : Star: Type ?u.24 β Type ?u.24Star (β i: ?m.26i, f: I β Type vf i: ?m.26i) where star x: ?m.37x i: ?m.40i := star: {R : Type ?u.42} β [self : Star R] β R β Rstar (x: ?m.37x i: ?m.40i)

@[simp]
theorem star_apply: β {I : Type u} {f : I β Type v} [inst : (i : I) β Star (f i)] (x : (i : I) β f i) (i : I), star x i = star (x i)star_apply [β i: ?m.177i, Star: Type ?u.180 β Type ?u.180Star (f: I β Type vf i: ?m.177i)] (x: (i : I) β f ix : β i: ?m.185i, f: I β Type vf i: ?m.185i) (i: Ii : I: Type uI) : star: {R : Type ?u.193} β [self : Star R] β R β Rstar x: (i : I) β f ix i: Ii = star: {R : Type ?u.231} β [self : Star R] β R β Rstar (x: (i : I) β f ix i: Ii) :=
rfl: β {Ξ± : Sort ?u.243} {a : Ξ±}, a = arfl
#align pi.star_apply Pi.star_apply: β {I : Type u} {f : I β Type v} [inst : (i : I) β Star (f i)] (x : (i : I) β f i) (i : I), star x i = star (x i)Pi.star_apply

theorem star_def: β [inst : (i : I) β Star (f i)] (x : (i : I) β f i), star x = fun i => star (x i)star_def [β i: ?m.283i, Star: Type ?u.286 β Type ?u.286Star (f: I β Type vf i: ?m.283i)] (x: (i : I) β f ix : β i: ?m.291i, f: I β Type vf i: ?m.291i) : star: {R : Type ?u.297} β [self : Star R] β R β Rstar x: (i : I) β f ix = fun i: ?m.337i => star: {R : Type ?u.339} β [self : Star R] β R β Rstar (x: (i : I) β f ix i: ?m.337i) :=
rfl: β {Ξ± : Sort ?u.353} {a : Ξ±}, a = arfl
#align pi.star_def Pi.star_def: β {I : Type u} {f : I β Type v} [inst : (i : I) β Star (f i)] (x : (i : I) β f i), star x = fun i => star (x i)Pi.star_def

instance: β {I : Type u} {f : I β Type v} [inst : (i : I) β Star (f i)] [inst_1 : β (i : I), TrivialStar (f i)],
TrivialStar ((i : I) β f i)instance [β i: ?m.381i, Star: Type ?u.384 β Type ?u.384Star (f: I β Type vf i: ?m.381i)] [β i: ?m.389i, TrivialStar: (R : Type ?u.392) β [inst : Star R] β PropTrivialStar (f: I β Type vf i: ?m.389i)] : TrivialStar: (R : Type ?u.404) β [inst : Star R] β PropTrivialStar (β i: ?m.406i, f: I β Type vf i: ?m.406i)
where star_trivial _: ?m.472_ := funext: β {Ξ± : Sort ?u.475} {Ξ² : Ξ± β Sort ?u.474} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext fun _: ?m.489_ => star_trivial: β {R : Type ?u.491} [inst : Star R] [self : TrivialStar R] (r : R), star r = rstar_trivial _: ?m.492_

instance: {I : Type u} β {f : I β Type v} β [inst : (i : I) β InvolutiveStar (f i)] β InvolutiveStar ((i : I) β f i)instance [β i: ?m.579i, InvolutiveStar: Type ?u.582 β Type ?u.582InvolutiveStar (f: I β Type vf i: ?m.579i)] : InvolutiveStar: Type ?u.586 β Type ?u.586InvolutiveStar (β i: ?m.588i, f: I β Type vf i: ?m.588i)
where star_involutive _: ?m.637_ := funext: β {Ξ± : Sort ?u.640} {Ξ² : Ξ± β Sort ?u.639} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext fun _: ?m.654_ => star_star: β {R : Type ?u.656} [inst : InvolutiveStar R] (r : R), star (star r) = rstar_star _: ?m.657_

instance: {I : Type u} β
{f : I β Type v} β
[inst : (i : I) β Semigroup (f i)] β [inst_1 : (i : I) β StarSemigroup (f i)] β StarSemigroup ((i : I) β f i)instance [β i: ?m.776i, Semigroup: Type ?u.779 β Type ?u.779Semigroup (f: I β Type vf i: ?m.776i)] [β i: ?m.784i, StarSemigroup: (R : Type ?u.787) β [inst : Semigroup R] β Type ?u.787StarSemigroup (f: I β Type vf i: ?m.784i)] : StarSemigroup: (R : Type ?u.803) β [inst : Semigroup R] β Type ?u.803StarSemigroup (β i: ?m.805i, f: I β Type vf i: ?m.805i)
where star_mul _: ?m.1997_ _: ?m.2000_ := funext: β {Ξ± : Sort ?u.2003} {Ξ² : Ξ± β Sort ?u.2002} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext fun _: ?m.2017_ => star_mul: β {R : Type ?u.2019} [inst : Semigroup R] [self : StarSemigroup R] (r s : R), star (r * s) = star s * star rstar_mul _: ?m.2020_ _: ?m.2020_

instance: {I : Type u} β
{f : I β Type v} β
where star_add _: ?m.2375_ _: ?m.2378_ := funext: β {Ξ± : Sort ?u.2381} {Ξ² : Ξ± β Sort ?u.2380} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext fun _: ?m.2395_ => star_add: β {R : Type ?u.2397} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star sstar_add _: ?m.2398_ _: ?m.2398_

instance: {I : Type u} β
{f : I β Type v} β
[inst : (i : I) β NonUnitalSemiring (f i)] β [inst_1 : (i : I) β StarRing (f i)] β StarRing ((i : I) β f i)instance [β i: ?m.2594i, NonUnitalSemiring: Type ?u.2597 β Type ?u.2597NonUnitalSemiring (f: I β Type vf i: ?m.2594i)] [β i: ?m.2602i, StarRing: (R : Type ?u.2605) β [inst : NonUnitalSemiring R] β Type ?u.2605StarRing (f: I β Type vf i: ?m.2602i)] : StarRing: (R : Type ?u.2619) β [inst : NonUnitalSemiring R] β Type ?u.2619StarRing (β i: ?m.2621i, f: I β Type vf i: ?m.2621i)
where star_add _: ?m.2858_ _: ?m.2861_ := funext: β {Ξ± : Sort ?u.2864} {Ξ² : Ξ± β Sort ?u.2863} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext fun _: ?m.2878_ => star_add: β {R : Type ?u.2880} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star sstar_add _: ?m.2881_ _: ?m.2881_

instance: β {I : Type u} {f : I β Type v} {R : Type w} [inst : (i : I) β SMul R (f i)] [inst_1 : Star R]
[inst_2 : (i : I) β Star (f i)] [inst_3 : β (i : I), StarModule R (f i)], StarModule R ((i : I) β f i)instance {R: Type wR : Type w: Type (w+1)Type w} [β i: ?m.3685i, SMul: Type ?u.3689 β Type ?u.3688 β Type (max?u.3689?u.3688)SMul R: Type wR (f: I β Type vf i: ?m.3685i)] [Star: Type ?u.3693 β Type ?u.3693Star R: Type wR] [β i: ?m.3697i, Star: Type ?u.3700 β Type ?u.3700Star (f: I β Type vf i: ?m.3697i)]
[β i: ?m.3705i, StarModule: (R : Type ?u.3709) β (A : Type ?u.3708) β [inst : Star R] β [inst : Star A] β [inst : SMul R A] β PropStarModule R: Type wR (f: I β Type vf i: ?m.3705i)] : StarModule: (R : Type ?u.3742) β (A : Type ?u.3741) β [inst : Star R] β [inst : Star A] β [inst : SMul R A] β PropStarModule R: Type wR (β i: ?m.3744i, f: I β Type vf i: ?m.3744i)
where star_smul r: ?m.3902r x: ?m.3905x := funext: β {Ξ± : Sort ?u.3908} {Ξ² : Ξ± β Sort ?u.3907} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext fun i: ?m.3922i => star_smul: β {R : Type ?u.3925} {A : Type ?u.3924} [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 r: ?m.3902r (x: ?m.3905x i: ?m.3922i)

theorem single_star: β [inst : (i : I) β AddMonoid (f i)] [inst_1 : (i : I) β StarAddMonoid (f i)] [inst_2 : DecidableEq I] (i : I)
(a : f i), single i (star a) = star (single i a)single_star [β i: ?m.4058i, AddMonoid: Type ?u.4061 β Type ?u.4061AddMonoid (f: I β Type vf i: ?m.4058i)] [β i: ?m.4066i, StarAddMonoid: (R : Type ?u.4069) β [inst : AddMonoid R] β Type ?u.4069StarAddMonoid (f: I β Type vf i: ?m.4066i)] [DecidableEq: Sort ?u.4085 β Sort (max1?u.4085)DecidableEq I: Type uI] (i: Ii : I: Type uI)
(a: f ia : f: I β Type vf i: Ii) : Pi.single: {I : Type ?u.4100} β
{f : I β Type ?u.4099} β [inst : DecidableEq I] β [inst : (i : I) β Zero (f i)] β (i : I) β f i β (j : I) β f jPi.single i: Ii (star: {R : Type ?u.4105} β [self : Star R] β R β Rstar a: f ia) = star: {R : Type ?u.5310} β [self : Star R] β R β Rstar (Pi.single: {I : Type ?u.5314} β
{f : I β Type ?u.5313} β [inst : DecidableEq I] β [inst : (i : I) β Zero (f i)] β (i : I) β f i β (j : I) β f jPi.single i: Ii a: f ia) :=
single_op: β {I : Type ?u.5492} {f : I β Type ?u.5491} [inst : DecidableEq I] [inst_1 : (i : I) β Zero (f i)]
{g : I β Type ?u.5493} [inst_2 : (i : I) β Zero (g i)] (op : (i : I) β f i β g i),
(β (i : I), op i 0 = 0) β β (i : I) (x : f i), single i (op i x) = fun j => op j (single i x j)single_op (fun i: ?m.5501i => @star: {R : Type ?u.5503} β [self : Star R] β R β Rstar (f: I β Type vf i: ?m.5501i) _) (fun _: ?m.5533_ => star_zero: β (R : Type ?u.5535) [inst : AddMonoid R] [inst_1 : StarAddMonoid R], star 0 = 0star_zero _: Type ?u.5535_) i: Ii a: f ia
#align pi.single_star Pi.single_star: β {I : Type u} {f : I β Type v} [inst : (i : I) β AddMonoid (f i)] [inst_1 : (i : I) β StarAddMonoid (f i)]
[inst_2 : DecidableEq I] (i : I) (a : f i), single i (star a) = star (single i a)Pi.single_star

end Pi

namespace Function

theorem update_star: β [inst : (i : I) β Star (f i)] [inst_1 : DecidableEq I] (h : (i : I) β f i) (i : I) (a : f i),
update (star h) i (star a) = star (update h i a)update_star [β i: ?m.6681i, Star: Type ?u.6684 β Type ?u.6684Star (f: I β Type vf i: ?m.6681i)] [DecidableEq: Sort ?u.6688 β Sort (max1?u.6688)DecidableEq I: Type uI] (h: (i : I) β f ih : β i: Ii : I: Type uI, f: I β Type vf i: Ii) (i: Ii : I: Type uI) (a: f ia : f: I β Type vf i: Ii) :
Function.update: {Ξ± : Sort ?u.6708} β {Ξ² : Ξ± β Sort ?u.6707} β [inst : DecidableEq Ξ±] β ((a : Ξ±) β Ξ² a) β (a' : Ξ±) β Ξ² a' β (a : Ξ±) β Ξ² aFunction.update (star: {R : Type ?u.6712} β [self : Star R] β R β Rstar h: (i : I) β f ih) i: Ii (star: {R : Type ?u.6765} β [self : Star R] β R β Rstar a: f ia) = star: {R : Type ?u.6820} β [self : Star R] β R β Rstar (Function.update: {Ξ± : Sort ?u.6824} β {Ξ² : Ξ± β Sort ?u.6823} β [inst : DecidableEq Ξ±] β ((a : Ξ±) β Ξ² a) β (a' : Ξ±) β Ξ² a' β (a : Ξ±) β Ξ² aFunction.update h: (i : I) β f ih i: Ii a: f ia) :=
funext: β {Ξ± : Sort ?u.6927} {Ξ² : Ξ± β Sort ?u.6926} {f g : (x : Ξ±) β Ξ² x}, (β (x : Ξ±), f x = g x) β f = gfunext fun j: ?m.6941j => (apply_update: β {ΞΉ : Sort ?u.6943} [inst : DecidableEq ΞΉ] {Ξ± : ΞΉ β Sort ?u.6944} {Ξ² : ΞΉ β Sort ?u.6945} (f : (i : ΞΉ) β Ξ± i β Ξ² i)
(g : (i : ΞΉ) β Ξ± i) (i : ΞΉ) (v : Ξ± i) (j : ΞΉ), f j (update g i v j) = update (fun k => f k (g k)) i (f i v) japply_update (fun _: ?m.6951_ => star: {R : Type ?u.6953} β [self : Star R] β R β Rstar) h: (i : I) β f ih i: Ii a: f ia j: ?m.6941j).symm: β {Ξ± : Sort ?u.7006} {a b : Ξ±}, a = b β b = asymm
#align function.update_star Function.update_star: β {I : Type u} {f : I β Type v} [inst : (i : I) β Star (f i)] [inst_1 : DecidableEq I] (h : (i : I) β f i) (i : I)
(a : f i), update (star h) i (star a) = star (update h i a)Function.update_star

theorem star_sum_elim: β {I : Type u_1} {J : Type u_2} {Ξ± : Type u_3} (x : I β Ξ±) (y : J β Ξ±) [inst : Star Ξ±],
star (Sum.elim x y) = Sum.elim (star x) (star y)star_sum_elim {I: Type u_1I J: Type ?u.7082J Ξ±: Type u_3Ξ± : Type _: Type (?u.7085+1)Type _} (x: I β Ξ±x : I: Type ?u.7079I β Ξ±: Type ?u.7085Ξ±) (y: J β Ξ±y : J: Type ?u.7082J β Ξ±: Type ?u.7085Ξ±) [Star: Type ?u.7096 β Type ?u.7096Star Ξ±: Type ?u.7085Ξ±] :
star: {R : Type ?u.7100} β [self : Star R] β R β Rstar (Sum.elim: {Ξ± : Type ?u.7105} β {Ξ² : Type ?u.7104} β {Ξ³ : Sort ?u.7103} β (Ξ± β Ξ³) β (Ξ² β Ξ³) β Ξ± β Ξ² β Ξ³Sum.elim x: I β Ξ±x y: J β Ξ±y) = Sum.elim: {Ξ± : Type ?u.7155} β {Ξ² : Type ?u.7154} β {Ξ³ : Sort ?u.7153} β (Ξ± β Ξ³) β (Ξ² β Ξ³) β Ξ± β Ξ² β Ξ³Sum.elim (star: {R : Type ?u.7159} β [self : Star R] β R β Rstar x: I β Ξ±x) (star: {R : Type ?u.7202} β [self : Star R] β R β Rstar y: J β Ξ±y) := byGoals accomplished! π
Iβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3x: I β Ξ±y: J β Ξ±instβ: Star Ξ±star (Sum.elim x y) = Sum.elim (star x) (star y)ext x: ?Ξ±xIβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3xβ: I β Ξ±y: J β Ξ±instβ: Star Ξ±x: I β Jhstar (Sum.elim xβ y) x = Sum.elim (star xβ) (star y) x;Iβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3xβ: I β Ξ±y: J β Ξ±instβ: Star Ξ±x: I β Jhstar (Sum.elim xβ y) x = Sum.elim (star xβ) (star y) x Iβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3x: I β Ξ±y: J β Ξ±instβ: Star Ξ±star (Sum.elim x y) = Sum.elim (star x) (star y)cases x: ?Ξ±xIβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3x: I β Ξ±y: J β Ξ±instβ: Star Ξ±valβ: Ih.inlstar (Sum.elim x y) (Sum.inl valβ) = Sum.elim (star x) (star y) (Sum.inl valβ)Iβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3x: I β Ξ±y: J β Ξ±instβ: Star Ξ±valβ: Jh.inrstar (Sum.elim x y) (Sum.inr valβ) = Sum.elim (star x) (star y) (Sum.inr valβ) Iβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3xβ: I β Ξ±y: J β Ξ±instβ: Star Ξ±x: I β Jhstar (Sum.elim xβ y) x = Sum.elim (star xβ) (star y) x<;>Iβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3x: I β Ξ±y: J β Ξ±instβ: Star Ξ±valβ: Ih.inlstar (Sum.elim x y) (Sum.inl valβ) = Sum.elim (star x) (star y) (Sum.inl valβ)Iβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3x: I β Ξ±y: J β Ξ±instβ: Star Ξ±valβ: Jh.inrstar (Sum.elim x y) (Sum.inr valβ) = Sum.elim (star x) (star y) (Sum.inr valβ) Iβ: Type uf: Iβ β Type vI: Type u_1J: Type u_2Ξ±: Type u_3xβ: I β Ξ±y: J β Ξ±instβ: Star Ξ±x: I β Jhstar (Sum.elim xβ y) x = Sum.elim (star xβ) (star y) xsimp only [Pi.star_apply: β {I : Type ?u.7374} {f : I β Type ?u.7373} [inst : (i : I) β Star (f i)] (x : (i : I) β f i) (i : I),
star x i = star (x i)Pi.star_apply, Sum.elim_inl: β {Ξ± : Type ?u.7703} {Ξ² : Type ?u.7704} {Ξ³ : Sort ?u.7705} (f : Ξ± β Ξ³) (g : Ξ² β Ξ³) (x : Ξ±),
Sum.elim f g (Sum.inl x) = f xSum.elim_inl, Sum.elim_inr: β {Ξ± : Type ?u.7719} {Ξ² : Type ?u.7720} {Ξ³ : Sort ?u.7721} (f : Ξ± β Ξ³) (g : Ξ² β Ξ³) (x : Ξ²),
Sum.elim f g (Sum.inr x) = g xSum.elim_inr]Goals accomplished! π
#align function.star_sum_elim Function.star_sum_elim: β {I : Type u_1} {J : Type u_2} {Ξ± : Type u_3} (x : I β Ξ±) (y : J β Ξ±) [inst : Star Ξ±],
star (Sum.elim x y) = Sum.elim (star x) (star y)Function.star_sum_elim

end Function
```