Introduction
1
Addenda to mathlib
▶
1.1
Group theory
▶
1.1.1
Two lemmas about the center of a group
1.1.2
Quotient of a group by its center
1.2
Direct sums and tensor products
▶
1.2.1
Direct sums
1.2.2
Tensor products
1.3
Group algebra
▶
1.3.1
Setting up operations, coercions and instances in LEAN
1.3.2
Splitting of a group algebra as a direct sum
1.4
Representation theory
▶
1.4.1
Building the induced representation
1.4.2
Character of the induced representation
2
Duality and conventions
▶
2.1
Setting up the conventions
2.2
Some results about the commutator bilinear form
3
Heisenberg’s group
▶
3.1
Construction
3.2
Center
3.3
Commutator and nilpotency
3.4
Short exact sequence
3.5
Specifities of the case \(k=\mathbb {F}_q\)
Dependency graph
Weil representations associated to finite fields
Parisot Loris
Introduction
1
Addenda to mathlib
1.1
Group theory
1.1.1
Two lemmas about the center of a group
1.1.2
Quotient of a group by its center
1.2
Direct sums and tensor products
1.2.1
Direct sums
1.2.2
Tensor products
1.3
Group algebra
1.3.1
Setting up operations, coercions and instances in LEAN
1.3.2
Splitting of a group algebra as a direct sum
1.4
Representation theory
1.4.1
Building the induced representation
1.4.2
Character of the induced representation
2
Duality and conventions
2.1
Setting up the conventions
2.2
Some results about the commutator bilinear form
3
Heisenberg’s group
3.1
Construction
3.2
Center
3.3
Commutator and nilpotency
3.4
Short exact sequence
3.5
Specifities of the case \(k=\mathbb {F}_q\)