Zulip Chat Archive

Stream: Is there code for X?

Topic: Swapping quotients


view this post on Zulip Jason KY. (Jan 31 2021 at 15:09):

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

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 04:35):

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


Last updated: May 16 2021 at 05:21 UTC