Opening Definitions

Stream: new members

[Brandon Sisler]

Hey y'all simple question. If I have the following defined a Semigroup, with Semigroup.mul_assoc how can I alter things so that I can just refer to it as mul_assoc. Thanks!

[Pedro Sánchez Terraf]

Inside the definition of docs#Semigroup, mul_assoc is “protected” (not accessible without the Semigroup. qualification). Nevertheless, you have the docs#mul_assoc theorem, which you invoke simply as such.

Perhaps if you provide a #mwe people will be able to help in a more focused way.

[Alex J. Best]

There is also the export command

import Mathlib


class Semigroup' where
  mul_assooc : True

#check mul_assooc

export Semigroup' (mul_assooc)

#check mul_assooc