instMonoHSMulHomOfInvertible — Mathlib

English

If f: X → Y is mono and r ∈ R is invertible, then r • f is mono.

Русский

Если морфизм f: X → Y моно и r обратим в R, то r • f снова моно.

LaTeX

$$$\\text{If } f \\text{ is mono and } r \\text{ invertible, then } r \\cdot f \\text{ is mono.}$$$

Lean4

instance {X Y : C} (f : X ⟶ Y) [Mono f] (r : R) [Invertible r] : Mono (r • f) :=
  ⟨fun g g' H => by
    rw [comp_smul, comp_smul, ← smul_comp, ← smul_comp, cancel_mono] at H
    simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H⟩

Похожие утверждения