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]
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_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
- 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)] :
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)
theorem
function.star_sum_elim
{I : Type u_1}
{J : Type u_2}
{α : Type u_3}
(x : I → α)
(y : J → α)
[has_star α] :
has_star.star (sum.elim x y) = sum.elim (has_star.star x) (has_star.star y)