mathlib3 documentation

algebra.star.pi

star on pi types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
has_star.star x = λ (i : I), has_star.star (x i)
@[protected, instance]
def pi.has_trivial_star {I : Type u} {f : I Type v} [Π (i : I), has_star (f i)] [ (i : I), has_trivial_star (f i)] :
has_trivial_star (Π (i : I), f 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), has_smul 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)
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) :
theorem function.star_sum_elim {I : Type u_1} {J : Type u_2} {α : Type u_3} (x : I α) (y : J α) [has_star α] :