Commit 2025-02-03 16:47 7bb96604

View on Github →

feat(Analysis/RCLike/Basic): PosMulReflectLE (#21351) Adds

@[simp]
theorem RCLike.inv_nonneg {x : 𝕜} : 0 ≤ x⁻¹ ↔ 0 ≤ x

to match inv_nonneg and Rat.inv_nonneg. Upstreamed from QuantumInfo

Estimated changes