mkq = 0 iff

Stream: Is there code for X?

[Scott Morrison]

import linear_algebra.quotient

lemma foo {R : Type*} [ring R] {M : Type*} [add_comm_group M] [module R M]
  (p : submodule R M) (x : M) : p.mkq x = 0 ↔ x ∈ p :=
sorry

This seems like a core part of the API for submodule.mpq, but I can't seem to find it ....? Any pointers?

[Riccardo Brasca]

docs#submodule.ker_mkq?

[Scott Morrison]

I guess that is the pointless version. :-)

[Scott Morrison]

I will add this later.

[Riccardo Brasca]

Ah ops! docs#submodule.quotient.mk_eq_zero then, but it uses quotient.mk

[Riccardo Brasca]

But the two are defeq, indeed

lemma foo {R : Type*} [ring R] {M : Type*} [add_comm_group M] [module R M]
  (p : submodule R M) (x : M) : p.mkq x = 0 ↔ x ∈ p :=
submodule.quotient.mk_eq_zero p

works.

[Scott Morrison]

Ah, I should have tried library_search!.

[Scott Morrison]

I added another copy of this lemma stated in terms of mkq so that simp can use it, in #12639.