Commit 2026-05-30 13:01 4d0d11cf
View on Github →chore: rename MonoidHom.injective_pi to pi_injective (#40045)
I introduced this name just a few hours ago, but I just realized that our naming convention explicitly states that it should be pi_injective.