Introduction

The main goal of this internship was to formalize some results of the paper "Weil Representation associated to finite fields" by P.Gérardin.

The first section of this report introduces some addenda to mathlib (or other formulations of existing results) that are mandatory to formalize the paper. Those results are about finite group theory, direct sums and tensor products and monoid algebra theory.
The second section aims to add results about the induced representation by the center of a finite group and to provides the formula for its character.
The third section corresponds to some parts of the paper : definition of Heisenberg’s group over vector spaces,...