English
A variant of the extension property parameterized by a motive relating g and h, using a matching morphism between extensions to guarantee existence of h with h ∘ f = g.
Русский
Вариант свойства расширения, параметризованный мотивом, связывающим g и h, с использованием соответствующего отображения между расширениями для обеспечения существования h с h ∘ f = g.
LaTeX
$$$ \\exists h' \\; \\text{such that } h' \\circ f = g $$$
Lean4
/-- **Baer's criterion** for injective module : a Baer module is an injective module, i.e. if every
linear map from an ideal can be extended, then the module is injective. -/
protected theorem injective (h : Module.Baer R Q) : Module.Injective R Q where
out X Y _ _ _ _ i hi
f := by
obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f
exact ⟨h, DFunLike.congr_fun H⟩
