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

• delta : ℂ
• delta_pos : 0 < delta A
• mul_comp_comul_eq : LinearMap.mul' ℂ A ∘ₗ CoalgebraStruct.comul = 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 ∘ₗ CoalgebraStruct.comul)

Equations

• QuantumSet.DeltaForm.mul_comp_comul_isInvertible = ⋯.invertible