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.

instance Pi.instStarForAll {I : Type u} {f : IType v} [inst : (i : I) → Star (f i)] :
Star ((i : I) → f i)
Equations
  • Pi.instStarForAll = { star := fun x i => star (x i) }
@[simp]
theorem Pi.star_apply {I : Type u} {f : IType v} [inst : (i : I) → Star (f i)] (x : (i : I) → f i) (i : I) :
star ((i : I) → f i) Pi.instStarForAll x i = star (x i)
theorem Pi.star_def {I : Type u} {f : IType v} [inst : (i : I) → Star (f i)] (x : (i : I) → f i) :
star x = fun i => star (x i)
instance Pi.instInvolutiveStarForAll {I : Type u} {f : IType v} [inst : (i : I) → InvolutiveStar (f i)] :
InvolutiveStar ((i : I) → f i)
Equations
instance Pi.instStarSemigroupForAllSemigroup {I : Type u} {f : IType v} [inst : (i : I) → Semigroup (f i)] [inst : (i : I) → StarSemigroup (f i)] :
StarSemigroup ((i : I) → f i)
Equations
instance Pi.instStarAddMonoidForAllAddMonoid {I : Type u} {f : IType v} [inst : (i : I) → AddMonoid (f i)] [inst : (i : I) → StarAddMonoid (f i)] :
StarAddMonoid ((i : I) → f i)
Equations
instance Pi.instStarRingForAllNonUnitalSemiring {I : Type u} {f : IType v} [inst : (i : I) → NonUnitalSemiring (f i)] [inst : (i : I) → StarRing (f i)] :
StarRing ((i : I) → f i)
Equations
instance Pi.instStarModuleForAllInstStarForAllInstSMul {I : Type u} {f : IType v} {R : Type w} [inst : (i : I) → SMul R (f i)] [inst : Star R] [inst : (i : I) → Star (f i)] [inst : ∀ (i : I), StarModule R (f i)] :
StarModule R ((i : I) → f i)
Equations
theorem Pi.single_star {I : Type u} {f : IType v} [inst : (i : I) → AddMonoid (f i)] [inst : (i : I) → StarAddMonoid (f i)] [inst : DecidableEq I] (i : I) (a : f i) :
theorem Function.update_star {I : Type u} {f : IType v} [inst : (i : I) → Star (f i)] [inst : DecidableEq 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α) [inst : Star α] :