Commit 2023-10-06 00:26 911cd305
View on Github →feat: first isomorphism theorem for rings (#7536) This matches the textbook version which does not assume surjectivity, and is also consistent with the Mathlib group theory version.
feat: first isomorphism theorem for rings (#7536) This matches the textbook version which does not assume surjectivity, and is also consistent with the Mathlib group theory version.