mathlib

fcaedc52 - feat(algebra/module): add injective module and Baer's criterion (#12895)

feat(algebra/module): add injective module and Baer's criterion (#12895) Baer's criterion for injective modules: if an $R$-module $M$ is such that every linear map from an ideal of $R$ to $M$ can be extended to $R\to M$, then $M$ is injective.