class QuantumSetDeltaForm (A : Type u_1) [starAlgebra A] [QuantumSet A] : Type

• delta : ℂ
• delta_pos : 0 < QuantumSetDeltaForm.delta A
• mul_comp_comul_eq : LinearMap.mul' ℂ A ∘ₗ Coalgebra.comul = QuantumSetDeltaForm.delta A • 1

theorem QuantumSetDeltaForm.delta_pos {A : Type u_1} : ∀ {inst : starAlgebra A} {inst_1 : QuantumSet A} [self : QuantumSetDeltaForm A], 0 < QuantumSetDeltaForm.delta A

theorem QuantumSetDeltaForm.mul_comp_comul_eq {A : Type u_1} : ∀ {inst : starAlgebra A} {inst_1 : QuantumSet A} [self : QuantumSetDeltaForm A], LinearMap.mul' ℂ A ∘ₗ Coalgebra.comul = QuantumSetDeltaForm.delta A • 1

noncomputable instance QuantumSet.DeltaForm.mul_comp_comul_isInvertible {A : Type u_1} [starAlgebra A] [QuantumSet A] [hA2 : QuantumSetDeltaForm A] : Invertible (LinearMap.mul' ℂ A ∘ₗ Coalgebra.comul)

Equations

• QuantumSet.DeltaForm.mul_comp_comul_isInvertible = ⋯.invertible