Linear Algebra and Groups

An experimental Lean repo exploring content which will be developed in the 2024 Linear Algebra and Groups course at Imperial College.

Online play

You can experiment with the material in this repository by running Lean in a web browser; this way you don't have to install anything.

Method 1: via Gitpod.

Just click here: . Note: the first time you run this, it might take 3-4 minutes to set up. Other times will be quicker.

When it looks like everything has downloaded, open up the LAGinLean directory (not the file!) and you should see some exercises.

Method 2: via Codespaces

Go to the project's home page on GitHub, click "Code" and then "Codespaces" so it looks like this:

Pic:

Then click on "create codespace on main", and then wait for a few minutes. When it looks like everything has downloaded, open up the LAGinLean directory (not the file!) and you should see some exercises.

Local installation

If you already have Lean and VS Code installed locally, just fire up VS Code, click on the upside-down A

and select Open Project -> Project: Download Project. Type in the following URL into the text box which appeared:

https://github.com/ImperialCollegeLondon/LAGinLean2024

and then select the directory where you want the project installed, type in the name of a folder you want to install the repo to, and then wait for a minute or two while everything downloads and compiles. Then accept the suggestion to open the course directory, and you should be up and running. Open up VS Code's file explorer (it looks like this)

then navigate to the LAGinLean directory (not the file!) and you should see some exercises.