Revision #2190 → #2854 · back to history
modifiedKadison–Schwarz inequality502cd9462937
| Field | From #2190 | To #2854 |
|---|
| note | No declaration for the Kadison–Schwarz inequality f(a)*f(a) ≤ f(a*a) for unital 2-positive maps was found in Mathlib. | No declaration for the Kadison–Schwarz inequality f(a)*f(a) ≤ f(a*a) for unital 2-positive maps was found in Mathlib (loogle "Kadison" returns zero hits). |
modifiedCallebaut's inequality4b7d3756281a
| Field | From #2190 | To #2854 |
|---|
| note | No declaration for Callebaut's inequality was found in Mathlib. | No declaration for Callebaut's inequality was found in Mathlib (loogle "Callebaut" returns zero hits). |
addedDot product on Rⁿfe2969439e9a
addedPositive linear functionaldc1b3a404dee
addedC*-algebra0970bcdb64cb