ClassFieldTheory.mem_fieldNormSubgroup_iff_ringEquiv
An element is a field norm exactly when its image under a compatible base-field equivalence is a field norm in the transported extension.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u v w xLean source · statement
theorem mem_fieldNormSubgroup_iff_ringEquiv
{F : Type u} {M : Type v} {F' : Type w} {M' : Type x}
[Field F] [Field M] [Field F'] [Field M']
[Algebra F M] [Algebra F' M']
[FiniteDimensional F M] [FiniteDimensional F' M']
(eF : F ≃+* F') (eM : M ≃+* M')
(he : (algebraMap F' M').comp eF.toRingHom =
eM.toRingHom.comp (algebraMap F M))
(a : Fˣ) :
a ∈ fieldNormSubgroup F M ↔
(Units.mapEquiv eF.toMulEquiv) a ∈ fieldNormSubgroup F' M'