Map from intersection

Stream: new members

[Ben McDonnell]

Hi, I'm trying to define a map from the intersection of two submodules. Let L and N be submodules of M. Then L \cap N is a submodule of M, and L\times N is a module. There is a map x : L \cap N to (x,x) : L \times N But I'm not sure how to lift x : L \cap N to x : L

[Johan Commelin]

I think you should use \glb instead of \cap. That way you invoke the lattice structure on submodules.

[Johan Commelin]

@Ben McDonnell The map from L \glb N to L is probably called inf_le_left.