Johan Commelin

Depends on #75 and #71

Depends on #72 and #77

This commit is generated using rg -l generalizedEigenspace | xargs sed -i 's/generalizedEigenspace/genEigenspace/g' rg -l maximalGeneralizedEigenspace | xargs sed -i 's/maximalGeneralizedEigenspace/maxGenEigenspace/g' The upshot is many shorter lemma names. --- [![Open...

PR into lwithfield-Lie-theorem

1

--- [](https://gitpod.io/from-referrer/)

* Brief instructions on how to use nightlies in `lean-toolchain`. * Pointer to https://leanprover-community.github.io/contribute/tags_and_branches.html with even more details.

The combined diff format is described here: https://git-scm.com/docs/git-diff#_combined_diff_format It is very useful for reviewing merge commits.

"CalcPanel" is not a supported Lean widget type.

1

I opened some PR in neovim and I got the following warning: ```text "CalcPanel" is not a supported Lean widget type. If you think it could be, please file an...

As part of the porting process to Lean 4, we should refactor mathlib to remove occurences of ```lean local attribute [semireducible] foobar attribute [irreducible] xyzzy ``` The following data is...

Hasse invariant of quadratic forms

1

https://en.wikipedia.org/wiki/Hasse_invariant_of_a_quadratic_form

We should define a boatload of predicates on `R ->+* S` There should be predicates on `variable (P : ∀ {R S : Type u} [comm_ring R] [comm_ring S] (f...