noncomputable instance tensorStarAlgebra {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] : starAlgebra (TensorProduct ℂ A B)

Equations

• tensorStarAlgebra = starAlgebra.mk (fun (r : ℝ) => AlgEquiv.TensorProduct.map (modAut r) (modAut r)) ⋯ ⋯

theorem modAut_tensor {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] (r : ℝ) : modAut r = AlgEquiv.TensorProduct.map (modAut r) (modAut r)

theorem modAut_tensor_tmul {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] (r : ℝ) (x : A) (y : B) : (modAut r) (x ⊗ₜ[ℂ] y) = (modAut r) x ⊗ₜ[ℂ] (modAut r) y

noncomputable instance instInnerProductAlgebraTensorProductComplex {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] : InnerProductAlgebra (TensorProduct ℂ A B)

Equations

• instInnerProductAlgebraTensorProductComplex = InnerProductAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance QuantumSet.tensorProduct {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] [h : Fact (k A = k B)] : QuantumSet (TensorProduct ℂ A B)

Equations

• QuantumSet.tensorProduct = QuantumSet.mk ⋯ (k A) ⋯ ⋯ (n A × n B) (instFintypeProd (n A) (n B)) inferInstance (onb.tensorProduct onb)

theorem QuantumSet.tensorProduct.k_eq₁ {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] [Fact (k A = k B)] : k (TensorProduct ℂ A B) = k A

theorem QuantumSet.tensorProduct.k_eq₂ {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] [h : Fact (k A = k B)] : k (TensorProduct ℂ A B) = k B

theorem comul_real {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] : Coalgebra.comul.real = ↑(TensorProduct.comm ℂ A A) ∘ₗ Coalgebra.comul