Theorems · Theorem · ring theory

Module.Baer.extension_property_addMonoidHom

∀ {Q : Type v} [inst : AddCommGroup Q] {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N], Module.Baer ℤ Q → ∀ (f : M →+ N), Function.Injective ⇑f → ∀ (g : M →+ Q), ∃ h, h.comp f = g

Defined in

Mathlib.Algebra.Module.Injective

Cited by

1 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupAddCommGroupAddCommGroup