Commit 2024-12-10 13:44 128f5afc

View on Github →

refactor(LocalRing/Basic): generalize to non-commutative (semi)rings (#18652) Small generalization of some Lemmas in LocalRing.Basic

Estimated changes

modified theorem IsLocalRing.of_surjective'