Commit 2025-01-22 16:20 184a325b

View on Github →

feat(Algebra/GroupWithZero): N⁰.comap f ≤ M⁰ for an injective f : M →*₀ N (#20955) Proofs of two facts about non-zero-divisors.

Estimated changes