Commit 2026-10-08 14:53 6be3d352
View on Github →refactor(RingTheory/FractionalIdeal): make spanSingleton a monoid with zero homomorphism (#44475)
FractionalIdeal.spanSingleton S is now a monoid with zero homomorphism P →*₀ FractionalIdeal S P.
The lemmas spanSingleton_zero, spanSingleton_one, spanSingleton_mul_spanSingleton and spanSingleton_pow are deprecated in favour of map_zero, map_one, map_mul and map_pow.
This was suggested by @tb65536 in #40636.
Prepared with Claude Code 🤖