Theorem IsStarProjection.add_sub_mul_of_commute

Modification history

2025-07-31 05:15
Mathlib/Algebra/Star/StarProjection.lean
feat(Algebra/Ring/Idempotent): subtraction lemmas for idempotents and star projections (#25910) …
Modified IsStarProjection.add_sub_mul_of_commuteView on Github →
2025-06-28 23:20
Mathlib/Algebra/Star/StarProjection.lean
feat(Algebra/Star/StarProjection): define star projections (#26052) …
Added IsStarProjection.add_sub_mul_of_commuteView on Github →