Swapping quotients

Stream: Is there code for X?

[Jason KY.]

Hi, does this definition exist in mathlib?

import linear_algebra.basic

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

def foo (P Q : submodule R M) (f : P.quotient ≃ₗ[R] Q) : Q.quotient ≃ₗ[R] P :=
begin
  sorry
end

[Yury G. Kudryashov]

This is false: take M = ℕ → R, P = {f | ∀ n, f (2 * n) = 0}, Q = ⊤.