Theorem IsStarProjection.two_mul_sub_one_mem_unitary

Modification history

2025-06-28 23:20
Mathlib/Algebra/Star/Unitary.lean
feat(Algebra/Star/StarProjection): define star projections (#26052) …
Added IsStarProjection.two_mul_sub_one_mem_unitaryView on Github →