Sublattice to lattice

Stream: new members

[Matúš Behun]

Anybody willing to point me at right direction? I am trying to make lattice from sublattice. As a template for creating sublattice I am using submonoid from src/group_theory/submonoid My code is here https://pastebin.com/raw/CAamfhHv

[Kevin Buzzard]

Do you have a question?

[Matúš Behun]

Yeah seems to me, by the output of infoview that I am missing some definition by the looking of output at info overview. I am still new to this and I am basically trying to copy functionality from here https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/submonoid/operations.lean#L326 but no clue. Even pointing me at documentation would help. Another question is this right approach to make sublattice definition for mathlib I would like to make pull request later on.

[Kevin Buzzard]

At first glance it looks great!

[Matúš Behun]

Thanks, but most of it is just appropriated code from submonoid.

[Matúš Behun]

Oh I probably get it now I am missing definition for function.injective.lattice

[Kevin Buzzard]

You randomly leave the sublattice namespace, so your ext and ext' are in the root namespace, which is not good.

[Matúš Behun]

thank you