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.

source
@[protected, 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
source
@[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)
source
theorem pi.star_def {I : Type u} {f : I → Type v} [Π (i : I), has_star (f i)] (x : Π (i : I), f i) :
star x = λ (i : I), star (x i)
source
@[protected, 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
source
@[protected, instance]
def pi.star_semigroup {I : Type u} {f : I → Type v} [Π (i : I), semigroup (f i)] [Π (i : I), star_semigroup (f i)] :
star_semigroup (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.star_add_monoid {I : Type u} {f : I → Type v} [Π (i : I), add_monoid (f i)] [Π (i : I), star_add_monoid (f i)] :
star_add_monoid (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.star_ring {I : Type u} {f : I → Type v} [Π (i : I), non_unital_semiring (f i)] [Π (i : I), star_ring (f i)] :
star_ring (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.star_module {I : Type u} {f : I → Type v} {R : Type w} [Π (i : I), has_scalar R (f i)] [has_star R] [Π (i : I), has_star (f i)] [∀ (i : I), star_module R (f i)] :
star_module R (Π (i : I), f i)