Theorems · Theorem · commutative algebra

Module.Presentation.CokernelData.mk.inj

∀ {A : Type u} {inst : Ring A} {M₁ : Type v₁} {M₂ : Type v₂} {inst_1 : AddCommGroup M₁} {inst_2 : Module A M₁}
  {inst_3 : AddCommGroup M₂} {inst_4 : Module A M₂} {pres₂ : Module.Presentation A M₂} {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} {lift : ι → pres₂.G →₀ A} {π_lift : ∀ (i : ι), pres₂.π (lift i) = f (g₁ i)} {lift_1 : ι → pres₂.G →₀ A}
  {π_lift_1 : ∀ (i : ι), pres₂.π (lift_1 i) = f (g₁ i)},
  { lift := lift, π_lift := π_lift } = { lift := lift_1, π_lift := π_lift_1 } → lift = lift_1

Defined in

Mathlib.Algebra.Module.Presentation.Cokernel

Cited by

1 results in Mathlib

Foundations

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