mathlib documentation

algebra.star.pi

star on pi types #

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

@[instance]
def pi.has_star {I : Type u} {f : I → Type v} [Π (i : I), has_star (f i)] :
has_star (Π (i : I), f i)
Equations
@[simp]
theorem pi.star_apply {I : Type u} {f : I → Type v} [Π (i : I), has_star (f i)] (x : Π (i : I), f i) (i : I) :
star x i = star (x i)
@[instance]
def pi.has_involutive_star {I : Type u} {f : I → Type v} [Π (i : I), has_involutive_star (f i)] :
has_involutive_star (Π (i : I), f i)
Equations
@[instance]
def pi.star_monoid {I : Type u} {f : I → Type v} [Π (i : I), monoid (f i)] [Π (i : I), star_monoid (f i)] :
star_monoid (Π (i : I), f i)
Equations
@[instance]
def pi.star_ring {I : Type u} {f : I → Type v} [Π (i : I), semiring (f i)] [Π (i : I), star_ring (f i)] :
star_ring (Π (i : I), f i)
Equations
@[instance]
def pi.star_algebra {I : Type u} {f : I → Type v} {R : Type w} [comm_semiring R] [Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] [star_ring R] [Π (i : I), star_ring (f i)] [Π (i : I), star_algebra R (f i)] :
star_algebra R (Π (i : I), f i)
Equations