KummerTheory.zHatUnit_padicCoordinate_isOfFinOrder_of_freeCoordinate_eq_zero
If the free p-adic coordinate of a profinite unit vanishes, its actual p-adic unit coordinate has finite order.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace KummerTheory
open ClassFormation
open LocalFieldTheory.PadicLean source · statement
theorem zHatUnit_padicCoordinate_isOfFinOrder_of_freeCoordinate_eq_zero
(u : ZHatˣ) (p : Nat.Primes)
(hfree :
zHatToPadicInt p
(Multiplicative.toAdd
(zHatUnitsDecomposition u).1) = 0) :
IsOfFinOrder
(zHatUnitsContinuousMulEquivPrimeProduct u p)