Commit 2026-06-03 15:07 51d2df2e
View on Github →chore: remove notations ^* and ^+ for fixed points (#40154)
Both notations are only used a few (2-3) times in Mathlib. Moreover, this hasn't been used at all in the last year.
In #39383 I suggested scoping the additive notation, but given how little it's used, I think it's better to delete this notation outright.