Theorem IsStarProjection.one_sub_mul_self

Modification history

2025-06-28 23:20

Mathlib/Algebra/Star/StarProjection.lean

feat(Algebra/Star/StarProjection): define star projections (#26052) …

Added IsStarProjection.one_sub_mul_self View on Github →