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
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