Theorems · Theorem · group theory

Monoid.PushoutI.of_injective

∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i},
  (∀ (i : ι), Function.Injective ⇑(φ i)) → ∀ (i : ι), Function.Injective ⇑(Monoid.PushoutI.of i)

All maps into the PushoutI, or amalgamated product of groups are injective, provided all maps in the diagram are injective. See also base_injective

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupGroup