Theorems · Theorem · category theory

MonoidHom.range_eq_top_of_cancel

∀ {A : Type u} {B : Type v} [inst : CommGroup A] [inst_1 : CommGroup 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

CommGroupCommGroup