FLT/Deformations/RepresentationTheory/Etale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Equivalence between continuous G-finite sets and k-etale algebras

The bulk of this development has been moved to FLT.Mathlib.* (see FLT.Mathlib.FieldTheory.Galois.Infinite and the files it imports). This file keeps only the convolution monoid structure on A →ₐ[K] L for a bialgebra A, which is not yet destined for Mathlib.

Imports (2)
Imported by 2 files
  1. instance (instance at line 30) line 30 source
  2. instance (instance at line 74) line 74 source