Inverses up to a scalar

If an element c of a commutative ring kills the kernel of a linear map f : M → N and b kills its cokernel, then f has an inverse up to b * c: there is a linear map g : N → M with f ∘ g = (b * c) • and g ∘ f = (b * c) •. The map is g n = c • m, where f m = b • n, built from the first isomorphism theorem LinearMap.quotKerEquivRange.

theorem LinearMap.exists_comp_eq_lsmul_of_mem_annihilator {A : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing A] [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) {b c : A} (hker : c ∈ Module.annihilator A ↥f.ker) (hcoker : b ∈ Module.annihilator A (N ⧸ f.range)) : ∃ (g : N →ₗ[A] M), f ∘ₗ g = (lsmul A N) (b * c) ∧ g ∘ₗ f = (lsmul A M) (b * c)

If c kills the kernel and b kills the cokernel of f : M → N, then f has an inverse up to b * c: some g : N → M satisfies f ∘ g = (b * c) • and g ∘ f = (b * c) •.