Issues

• Questions about definition of a KET

  question
  Timeroot/Lean-QuantumInfo#18 · Filter by author swiswioo24 opened on Oct 23, 2025
  1

• Switch CPTPMap + more to "___Class"

  tech-debt
  Timeroot/Lean-QuantumInfo#13 · Filter by author Timeroot opened on Jun 12, 2025

• Switch Bra/Ket to use EuclideanSpace

  tech-debt
  Timeroot/Lean-QuantumInfo#12 · Filter by author Timeroot opened on Jun 12, 2025
  

• Data Processing Inequality

  theorem-wishlist
  Timeroot/Lean-QuantumInfo#10 · Filter by author Timeroot opened on Jun 12, 2025

• Strong Subadditivity

  theorem-wishlist
  Timeroot/Lean-QuantumInfo#9 · Filter by author Timeroot opened on Jun 12, 2025

• Subadditivity of von Neumann Entropy

  theorem-wishlist
  Timeroot/Lean-QuantumInfo#8 · Filter by author Timeroot opened on Jun 12, 2025