Repository navigation

Import brauergroup_new formalization - #88

Merged

Vilin97 merged 38 commits into

mainfrom

import/brauergroup_new

Jun 1, 2026

Merged

Import brauergroup_new formalization#88
Vilin97 merged 38 commits into
mainfrom
import/brauergroup_new

Commits on May 17, 2026
- Vendor Brauer group core
  Vilin97
  committed
  bf80767
Commits on May 18, 2026
- Merge branch 'main' into import/brauergroup_new
  Vilin97
  authored
  ce6d0f0
- Add Brauer group source citation
  Vilin97
  committed
  971b78b
- Regenerate project card
  Vilin97
  committed
  a56d88f
Commits on May 19, 2026
- Add Brauer group core
  Vilin97
  committed
  14c2b52
- Narrow Brauer group source scope
  Vilin97
  committed
  020f677
- Merge origin/main into import/brauergroup_new
  Vilin97
  committed
  e8ef5ac
Commits on May 20, 2026
- Restore BrauerGroup finite-field theorem
  Vilin97
  committed
  68df6f3
Commits on May 21, 2026
- Merge remote-tracking branch 'origin/main' into import/brauergroup_new
  Vilin97
  committed
  d849a45
Commits on May 24, 2026
- Add BrauerGroup upstream repository metadata
  Vilin97
  committed
  e471ca7
- Restore BrauerGroup upstream helper files
  Vilin97
  committed
  615ae54
- Restore BrauerGroup Morita equivalence
  Vilin97
  committed
  1c3f64b
- Restore BrauerGroup splitting prerequisites
  Vilin97
  committed
  649db4d
- Restore BrauerGroup helper compatibility modules
  Vilin97
  committed
  50a106f
- Port BrauerGroup ZeroSevenFourE
  Vilin97
  committed
  a82b595
- Port BrauerGroup Skolem-Noether
  Vilin97
  committed
  e937e58
- Port BrauerGroup double centralizer
  Vilin97
  committed
  b4642f2
- Port BrauerGroup maximal subfields
  Vilin97
  committed
  8910b16
- Port relative Brauer group
  Vilin97
  committed
  23158bc
- Port BrauerGroup subfield splitting
  Vilin97
  committed
  06f9aab
- Port BrauerGroup cross product algebra
  Vilin97
  committed
  daac4e1
- Port BrauerGroup Morita change of rings
  Vilin97
  committed
  032d6f2
- Port BrauerGroup Azumaya basics
  Vilin97
  committed
  8f3190a
- Port BrauerGroup Azumaya multiplication
  Vilin97
  committed
  9aa75f4
- Fix BrauerGroup Azumaya warning-free build
  Vilin97
  committed
  01933f8
- Port BrauerGroup Morita tensor product
  Vilin97
  committed
  cc173b4
- Port BrauerGroup ShortComplex homology example
  Vilin97
  committed
  08d7bfe
Commits on May 25, 2026
- Port BrauerGroup second cohomology equivalence
  Vilin97
  committed
  1ce8ea6
- Port BrauerGroup additive cohomology isomorphism
  Vilin97
  committed
  bb8843d
- Port BrauerGroup Frobenius theorem
  Vilin97
  committed
  275547d
- Port BrauerGroup separable subfields
  Vilin97
  committed
  a415b60
- Port BrauerGroup real and absolute results
  Vilin97
  committed
  02c6f33
- Restore BrauerGroup compatibility declarations
  Vilin97
  committed
  4dc2d5b
- Restore BrauerGroup congruence compatibility import
  Vilin97
  committed
  9d7c140
- Restore BrauerGroup tensor compatibility helper
  Vilin97
  committed
  5e9435c
- Use Mathlib span compatibility theorem
  Vilin97
  committed
  1b75fcf
- Clean BrauerGroup separable subfield warnings
  Vilin97
  committed
  8445168
Commits on Jun 1, 2026
- Merge remote-tracking branch 'origin/main' into tmp-brauergroup_new
  Vilin97
  committed
  b2b05d5

Commits

Commits on May 17, 2026

Commits on May 18, 2026

Commits on May 19, 2026

Commits on May 20, 2026

Commits on May 21, 2026

Commits on May 24, 2026

Commits on May 25, 2026

Commits on Jun 1, 2026