Theorem IsStarProjection.sub_iff_mul_eq_left

Modification history

2025-07-31 05:15
Mathlib/Algebra/Star/StarProjection.lean
feat(Algebra/Ring/Idempotent): subtraction lemmas for idempotents and star projections (#25910) …
Added IsStarProjection.sub_iff_mul_eq_leftView on Github →