The level-zero factor is trivial. At every positive level, the finite-place character specification reduces the claim to the ramified chosen-Artin formula proved in RationalCyclotomicFinitePlaceArtin.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocityinstance (p : Nat.Primes) : Fact p.1.PrimeThe chosen finite-place factor at the ramified prime p is the direct reduction of the rational p-adic unit.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalCyclotomicPrincipalFinitePlaceCharacter_at_prime
(p : Nat.Primes) (k : ℕ) (x : ℚˣ) :
rationalCyclotomicPrincipalFinitePlaceCharacter p k x p =
Units.map (PadicInt.toZModPow k).toMonoidHom
(padicIntUnitOfRat p
(rationalPrimeUnit x p : ℚ)
(rationalPrimeUnit x p).ne_zero
(padicValRat_rationalPrimeUnit x p))