Namespace `TWLoc` 1 theorems

Frobenius conjugation is q-th power on inertia, up to wild part TWLoc.frobenius_conj_mul_pow_inv_wild 4 below · cited by 2 · depth 11

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.

Namespace TWLoc 1 theorems

Namespace `TWLoc` 1 theorems