instantiation

Stream: new members

[亚历山大大帝]

How can we instantiate Group (↥P ⊔ ↥Q)? In Lean, does instantiating Group require formalizing all the theorems it satisfies in code?

[Edward van de Meent]

could you post a #mwe?

[Edward van de Meent]

in particular, i'm curious how you got ↥P ⊔ ↥Q... because from the looks of it you're taking the maximum of types, rather than of subgroups/subring/whatever

[Kevin Buzzard]

#mwe is a link containing the information we want. Right now your questions are impossible to answer because we don't have enough information in the question, we need to see the types of everything.