Formalising Brauer Group and Group Cohomology in Lean4

The concept of Brauer Groups, originally developed to classify division algebras, has now found many uses in scheme theory and class field theory. Brauer Groups over a field k is defined as the collection of central simple
algebras over k modulo certain equivalence relations and this project is set out to formalise the correspondence between the Brauer groups and the second
Galois cohomology groups Br(k) ≅ H²(Gal(k_sep/k) , k ⃰_sep). In this talk, we give a complete formalisation between the relative Brauer group of a finite
dimensional field extension Br(K/k) and the second group cohomology H²(Gal (K/k) , K ⃰) as the first step.

Github Repository: https://github.com/Whysoserioushah/BrauerGroup_new