trivial kernel of injective monoid_hom

Stream: new members

[Yakov Pechersky]

For a ->+ that is proven to be injective, what's the name of the lemma that the kernel is trivial? Specifically, I'm looking to prove this iff in a neat way

import group_theory.perm.basic

open equiv

variables {α β : Type*} {p : β → Prop} [decidable_pred p]

lemma extend_domain_eq_one_iff {e : perm α} {f : α ≃ subtype p} :
  e.extend_domain f = 1 ↔ e = 1 :=
begin
end

[Yakov Pechersky]

Ah, monoid_hom.injective_iff.

[Yakov Pechersky]

Is there a reason why the RHS of the iff is in implication form instead of iff?

[Eric Wieser]

docs#monoid_hom.injective_iff

[Eric Wieser]

It's probably because if the RHS were an iff, then rw injective_iff leaves you a goal with more to clean up.