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.

@[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
@[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) :
theorem pi.star_def {I : Type u} {f : I → Type v} [Π (i : I), has_star (f i)] (x : Π (i : I), f i) :
= λ (i : I), has_star.star (x i)
@[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
@[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
@[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
@[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
@[protected, instance]
def pi.star_module {I : Type u} {f : I → Type v} {R : Type w} [Π (i : I), (f i)] [has_star R] [Π (i : I), has_star (f i)] [∀ (i : I), (f i)] :
(Π (i : I), f i)
theorem pi.single_star {I : Type u} {f : I → Type v} [Π (i : I), add_monoid (f i)] [Π (i : I), star_add_monoid (f i)] [decidable_eq I] (i : I) (a : f i) :
theorem function.update_star {I : Type u} {f : I → Type v} [Π (i : I), has_star (f i)] [decidable_eq I] (h : Π (i : I), f i) (i : I) (a : f i) :