Theorem mul_one_sub_mul

Modification history

2026-04-28 22:33
Mathlib/Algebra/Ring/Defs.lean
feat(Analysis/CStarAlgebra): set of star projections equals the extreme points of the nonnegative closed unit ball (#36201) …
Added mul_one_sub_mulView on Github →