ClassFieldTheory.RayClassFieldRealization.rayArtin
The Frobenius-normalized ray Artin map.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory.RayClassFieldRealization
universe uLean source · statement
def rayArtin
{K : Type u} [Field K] [NumberField K]
{m : RayClassModulus K}
(R : RayClassFieldRealization K m) :
RayClassGroup m →* (R.extension ≃ₐ[K] R.extension)