Documentation

Monlib.LinearAlgebra.QuantumSet.Pi

@[reducible, inline]
abbrev PiQ {ι : Type u_1} (A : ιType u_3) [Fintype ι] [(i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] :
Type (max u_1 u_3)
Equations
Instances For
    @[defaultInstance 1000]
    instance instRingPiQ {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] :
    Ring (PiQ A)
    Equations
    @[defaultInstance 1000]
    instance instAlgebraComplexPiQ {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] :
    Equations
    @[defaultInstance 1000]
    instance instStarRingPiQ {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] :
    Equations
    @[defaultInstance 1000]
    instance instStarModuleComplexPiQ {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] :
    theorem PiLp.mul_apply {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (x y : PiQ A) (i : ι) :
    (x * y) i = x i * y i
    def Pi.modAut {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (r : ) :
    Equations
    Instances For
      theorem Pi.modAut_apply {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (r : ) (x : PiQ A) (i : ι) :
      (modAut r) x i = (starAlgebra.modAut r) (x i)
      instance piStarAlgebra {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] :
      Equations
      theorem piStarAlgebra.modAut {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (r : ) (x : PiQ A) (i : ι) :
      noncomputable instance piInnerProductAlgebra {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] :
      Equations
      theorem piInnerProductAlgebra.inner_apply {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [(i : ι) → QuantumSet (A i)] (a b : PiQ A) :
      inner a b = i : ι, inner (a i) (b i)
      noncomputable instance Pi.quantumSet {ι : Type u_1} {A : ιType u_2} [Fintype ι] [hA : (i : ι) → starAlgebra (A i)] [hA✝ : (i : ι) → QuantumSet (A i)] [gns : Fact (∀ (i : ι), k (A i) = 0)] :
      Equations