IMO 1982 Q3

Stream: new members

[Alex Brodbelt]

I have never made a PR before and would like to contribute this to the collection of formalised IMO problems

https://github.com/AlexBrodbelt/LeanIMO/tree/main/Imo1982Q3

how do I proceed?

[Luigi Massacci]

See here: https://leanprover-community.github.io/contribute/index.html

[Luigi Massacci]

See here: https://leanprover-community.github.io/contribute/index.html

[Alex Brodbelt]

Luigi Massacci said:

See here: https://leanprover-community.github.io/contribute/index.html

Thanks!
I have followed instructions and pushed changes to a branch on my forked version of mathlib.
It says I need to ask for request access to non-master branches

[Luigi Massacci]

As the link I sent you says, you should ask for it on Zulip ; ) For example here: #mathlib4 > github permission

[Luigi Massacci]

You can’t push from forks though for CI reasons (says that too… ; )

[Luigi Massacci]

(deleted)

[Luigi Massacci]

(also I forgot to say, but good work on the formalisation!)

[Alex Brodbelt]

Thanks for the help, sorry for being a bit useless

[Alex Brodbelt]

Luigi Massacci said:

(also I forgot to say, but good work on the formalisation!)

Thanks!!