star on pi types

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

ink

instance Pi.instStarForAll {I : Type u} {f : I → Type v} [inst : (i : I) → Star (f i)] : Star ((i : I) → f i)

Equations

• Pi.instStarForAll = { star := fun x i => star (x i) }

ink

@[simp]

theorem Pi.star_apply {I : Type u} {f : I → Type v} [inst : (i : I) → Star (f i)] (x : (i : I) → f i) (i : I) : star ((i : I) → f i) Pi.instStarForAll x i = star (x i)

ink

theorem 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)

ink

instance Pi.instInvolutiveStarForAll {I : Type u} {f : I → Type v} [inst : (i : I) → InvolutiveStar (f i)] : InvolutiveStar ((i : I) → f i)

Equations

• Pi.instInvolutiveStarForAll = InvolutiveStar.mk (_ : ∀ (x : (i : I) → f i), star (star x) = x)

ink

instance Pi.instStarSemigroupForAllSemigroup {I : Type u} {f : I → Type v} [inst : (i : I) → Semigroup (f i)] [inst : (i : I) → StarSemigroup (f i)] : StarSemigroup ((i : I) → f i)

Equations

• Pi.instStarSemigroupForAllSemigroup = StarSemigroup.mk (_ : ∀ (x x_1 : (i : I) → f i), star (x * x_1) = star x_1 * star x)

ink

instance Pi.instStarAddMonoidForAllAddMonoid {I : Type u} {f : I → Type v} [inst : (i : I) → AddMonoid (f i)] [inst : (i : I) → StarAddMonoid (f i)] : StarAddMonoid ((i : I) → f i)

Equations

• Pi.instStarAddMonoidForAllAddMonoid = StarAddMonoid.mk (_ : ∀ (x x_1 : (i : I) → f i), star (x + x_1) = star x + star x_1)

ink

instance Pi.instStarRingForAllNonUnitalSemiring {I : Type u} {f : I → Type v} [inst : (i : I) → NonUnitalSemiring (f i)] [inst : (i : I) → StarRing (f i)] : StarRing ((i : I) → f i)

Equations

• Pi.instStarRingForAllNonUnitalSemiring = StarRing.mk (_ : ∀ (x x_1 : (i : I) → f i), star (x + x_1) = star x + star x_1)

ink

instance Pi.instStarModuleForAllInstStarForAllInstSMul {I : Type u} {f : I → Type v} {R : Type w} [inst : (i : I) → SMul R (f i)] [inst : Star R] [inst : (i : I) → Star (f i)] [inst : ∀ (i : I), StarModule R (f i)] : StarModule R ((i : I) → f i)

Equations

• @Pi.instStarModuleForAllInstStarForAllInstSMul = @Pi.instStarModuleForAllInstStarForAllInstSMul.proof_1

ink

theorem Pi.single_star {I : Type u} {f : I → Type v} [inst : (i : I) → AddMonoid (f i)] [inst : (i : I) → StarAddMonoid (f i)] [inst : DecidableEq I] (i : I) (a : f i) : Pi.single i (star a) = star (Pi.single i a)

ink

theorem Function.update_star {I : Type u} {f : I → Type v} [inst : (i : I) → Star (f i)] [inst : DecidableEq I] (h : (i : I) → f i) (i : I) (a : f i) : Function.update (star h) i (star a) = star (Function.update h i a)

ink

theorem 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)