star
on pi types #
We put a Star
structure on pi types that operates elementwise, such that it describes the
complex conjugation of vectors.
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)
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)
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)
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)
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)
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)
:
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)