Registry · Theorem III.T37 tau-effective formalized

III.T37 — Base Change-Transfer Naturality

Base change (Enr₀₁ on sector morphisms) and transfer (defect functional between sectors) are natural transformations on the enriched bi-square

Book III Part 6 Ch. 49

Dependency Graph

Depends on (2)

III.T36 III.D57

Depended on by (2)

III.D65 III.T40

Lean Formalization

Module: TauLib.BookIII.Arithmetic.Langlands

Symbol: base_change_check