Documentation

Mathlib.Algebra.Star.Pi

star on pi types #

We put a Star structure on pi types that operates elementwise, such that it describes the complex conjugation of vectors.

source
instance Pi.instStarForall {I : Type u} {f : I → Type v} [(i : I) → Star (f i)] :
Star ((i : I) → f i)
Equations
    source
    @[simp]
    theorem Pi.star_apply {I : Type u} {f : I → Type v} [(i : I) → 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) → Star (f i)] (x : (i : I) → f i) :
    star x = fun (i : I) => star (x i)
    source
    instance Pi.instTrivialStarForall {I : Type u} {f : I → Type v} [(i : I) → Star (f i)] [∀ (i : I), TrivialStar (f i)] :
    TrivialStar ((i : I) → f i)
    source
    instance Pi.instInvolutiveStarForall {I : Type u} {f : I → Type v} [(i : I) → InvolutiveStar (f i)] :
    InvolutiveStar ((i : I) → f i)
    Equations
      source
      instance Pi.instStarMulForall {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] [(i : I) → StarMul (f i)] :
      StarMul ((i : I) → f i)
      Equations
        source
        instance Pi.instStarAddMonoidForall {I : Type u} {f : I → Type v} [(i : I) → AddMonoid (f i)] [(i : I) → StarAddMonoid (f i)] :
        StarAddMonoid ((i : I) → f i)
        Equations
          source
          instance Pi.instStarRingForall {I : Type u} {f : I → Type v} [(i : I) → NonUnitalSemiring (f i)] [(i : I) → StarRing (f i)] :
          StarRing ((i : I) → f i)
          Equations
            source
            instance Pi.instStarModuleForall {I : Type u} {f : I → Type v} {R : Type w} [(i : I) → SMul R (f i)] [Star R] [(i : I) → Star (f i)] [∀ (i : I), StarModule R (f i)] :
            StarModule R ((i : I) → f i)
            source
            theorem Pi.single_star {I : Type u} {f : I → Type v} [(i : I) → AddMonoid (f i)] [(i : I) → StarAddMonoid (f i)] [DecidableEq I] (i : I) (a : f i) :
            single i (star a) = star (single i a)
            source
            @[simp]
            theorem Pi.conj_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CommSemiring (α i)] [(i : ι) → StarRing (α i)] (f : (i : ι) → α i) (i : ι) :
            (starRingEnd ((i : ι) → α i)) f i = (starRingEnd (α i)) (f i)
            source
            theorem Function.update_star {I : Type u} {f : I → Type v} [(i : I) → Star (f i)] [DecidableEq I] (h : (i : I) → f i) (i : I) (a : f i) :
            update (star h) i (star a) = star (update h i a)
            source
            theorem Function.star_sumElim {I : Type u_1} {J : Type u_2} {α : Type u_3} (x : I → α) (y : J → α) [Star α] :
            star (Sum.elim x y) = Sum.elim (star x) (star y)
            source
            @[deprecated Function.star_sumElim (since := "2025-02-21")]
            theorem Function.star_sum_elim {I : Type u_1} {J : Type u_2} {α : Type u_3} (x : I → α) (y : J → α) [Star α] :
            star (Sum.elim x y) = Sum.elim (star x) (star y)

            Alias of Function.star_sumElim.