Theorems · Theorem · category theory

AddMonoidHom.range_eq_top_of_cancel

∀ {A : Type u} {B : Type v} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] {f : A →+ B},
  (∀ (u v : B →+ B ⧸ f.range), u.comp f = v.comp f → u = v) → f.range = ⊤

Defined in

Mathlib.Algebra.Category.Grp.EpiMono

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupAddCommGroup