search

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 298 forks source link

Hasse invariant of quadratic forms #3082

Open jcommelin opened 4 years ago

jcommelin commented 4 years ago

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

kbuzzard commented 2 years ago

@101damnations is working on group cohomology which is a prerequisite for doing this "properly".