Registry · Proposition III.P28 tau-effective formalized

III.P28 — Duality as Mutual Determination on ℤ²

Automorphic-Galois duality is Mutual Determination with m-axis as boundary, n-axis as spectral, full character as interior

Book III Part 6 Ch. 48

Dependency Graph

Depends on (2)

III.D63 III.D64

Depended on by (2)

III.T36 III.T40

Lean Formalization

Module: TauLib.BookIII.Arithmetic.Langlands

Symbol: duality_md_check