Get started with Lean 3

Stream: general

[Martin Dvořák]

Could this page indicate that it is written for Lean 3 please?
https://leanprover-community.github.io/get_started.html

[Kevin Buzzard]

You can probably make the PR yourself (but I'm not sure which repo it is)

[Martin Dvořák]

I already made a PR with the same suggestion to a different page in the same repository, but nobody merged it. I guess I must ask the right people?

[Eric Wieser]

You should ping those PRs on #PR reviews, very few people check the PRs on repos that aren't mathlib