KummerTheory.zHatUnitsDecomposition_freeCoordinate
The p-adic coordinate of the global free factor in zHatUnitsDecomposition is exactly the free factor in the genuine local decomposition of the p-adic unit coordinate.
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 zHatUnitsDecomposition_freeCoordinate
(u : ZHatˣ) (p : Nat.Primes) :
zHatToPadicInt p
(Multiplicative.toAdd
(zHatUnitsDecomposition u).1) =
Multiplicative.toAdd
(((padicUnitDecomposition p.1).symm
(zHatUnitsContinuousMulEquivPrimeProduct u p)).2)