Q is injective

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have the fact that $\mathbb{Q}$ (or any divisible abelian group for that matter) is an injective object in the category of abelian groups? I'm not necessarily looking for the categorical statement, but rather a lemma saying that I can extend a morphism $H \to \mathbb{Q}$ from a subgroup $H$ of $A$ to a morphism from all of $A$.

[Eric Wieser]

I assume you mean (H : add_subgroup A) (f : H →+ ℚ) : A →+ ℚ?

[Kevin Buzzard]

Proof by Zorn. You can always extend to an element not in the domain