First isomorphism theorem for modules (source code)

= First isomorphism theorem for modules
{title2=$M/\ker f\cong\operatorname{Im}f$}

For a <module homomorphism> $f:M\to N$, the map $m+\ker f\mapsto f(m)$ is a <module isomorphism> $M/\ker f\to\operatorname{Im}f$. The formula is well-defined because two representatives differ by an element of the <kernel of a module homomorphism> exactly when their images agree; the same observation proves injectivity, and surjectivity onto the image follows by its definition.