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.

Note that pi.star_algebra is in a different file to avoid pulling in everything from algebra/algebra/basic.

@[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