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
- pi.has_star = {star := λ (x : Π (i : I), f i) (i : I), has_star.star (x i)}
@[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) :
has_star.star x i = has_star.star (x 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_involutive_star
{I : Type u}
{f : I → Type v}
[Π (i : I), has_involutive_star (f i)] :
has_involutive_star (Π (i : I), f i)
Equations
- pi.has_involutive_star = {to_has_star := pi.has_star (λ (i : I), has_involutive_star.to_has_star), star_involutive := _}
@[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
- pi.star_semigroup = {to_has_involutive_star := pi.has_involutive_star (λ (i : I), star_semigroup.to_has_involutive_star), star_mul := _}
@[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
- pi.star_add_monoid = {to_has_involutive_star := pi.has_involutive_star (λ (i : I), star_add_monoid.to_has_involutive_star), star_add := _}
@[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) :
pi.single i (has_star.star a) = has_star.star (pi.single i a)
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) :
function.update (has_star.star h) i (has_star.star a) = has_star.star (function.update h i a)