cyclotomic character as (L ≃ₐ[K] L) →* ℤ_[p]ˣ

Stream: mathlib4

[Jz Pan]

What is the correct spelling of it? Is it (cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut (L ≃ₐ[K] L) L) as in cyclotomicCharacter.continuous? Should we add a def/abbrev to it? I'd like to prove the fact that if $L=K(\mu_{p^\infty})$, then such map is injective.