Module docstring incorrectly claims coverage of α-Renyi entropy

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it.

Summary

The documentation in QuantumInfo/Entropy/Axiomatized/Renyi.lean (around line 10) is incorrect.

Current text

/-! # Quantum Relative Entropy and α-Renyi Entropy -/

Why this is wrong

The module docstring for physlib/QuantumInfo/Entropy/Axiomatized/Renyi.lean states that the file covers both quantum relative entropy and α-Rényi entropy. However, the file only contains definitions and theorems related to quantum relative entropy via the declaration qRelativeEnt, with no mention of α-Rényi entropy anywhere in the code.

This discrepancy is incorrect because the code does not define or reference any α-Rényi entropy constructs. The correction removes the false claim about α-Rényi entropy, aligning the documentation with the actual content of the file. The remaining text accurately describes the sole focus on quantum relative entropy, as evidenced by the qRelativeEnt definition and associated theorems.

Suggested correction

/-! # Quantum Relative Entropy -/

Open QuantumInfo/Entropy/Axiomatized/Renyi.lean around line 10 and compare the module docstring with the file's qRelativeEnt-related content. Update the heading so it describes only quantum relative entropy, then verify that the α-Rényi entropy claim is gone.