Registry · Definition
I.D38
tau-effective
formalized
I.D38 — Character Group
The set of all characters on L with pointwise multiplication. Every character traces back to the bipolar partition of primes.
Dependency Graph
Depends on (1)
Depended on by (2)
Lean Formalization
Module: TauLib.BookI.Boundary.Characters
Symbol: Tau.Boundary.chi_complete