Morphism_Property_Preserves_Cancellability
Provedcancellabilityhomomorphismsproofwiki
If f is an injective homomorphism and a is cancellable, then f(a) is cancellable in the image.
Preamble
import Mathlib.Data.Set.Function import Mathlib.Algebra.Group.Defs
Formal statement
theorem Morphism_Property_Preserves_Cancellability {G H : Type _} [Mul G] [Mul H] (f : G → H) (hf : ∀ a b : G, f (a * b) = f a * f b) (hinj : Function.Injective f) (a : G) (hla : ∀ x y : G, a * x = a * y → x = y) : ∀ x y : H, x ∈ Set.range f → y ∈ Set.range f → f a * x = f a * y → x = y := by sorrySource