NYLL
Module

FieldNormEquiv.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FieldNormEquiv
2 declarations indexed from sourceView source ↗

Module documentation

Field-norm subgroups under algebra equivalence

An algebra equivalence over the base field preserves the field norm and therefore identifies the corresponding norm subgroups of the base unit group.

Imports1
Imported by1

Declarations

theorem

fieldNormUnits_map_algEquiv

L29 ↗
LocalFieldTheory.DiscreteValuationField.fieldNormUnits_map_algEquiv
Documentation

Mapping a unit through a base-field algebra equivalence does not change its field norm.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w
namespace LocalFieldTheory.DiscreteValuationField
variable (K : Type u) (L : Type v) (E : Type w)
variable [Field K] [Field L] [Field E]
variable [Algebra K L] [Algebra K E]
Lean source · statement
theorem fieldNormUnits_map_algEquiv
    (e : L ≃ₐ[K] E) (z : Lˣ) :
    normUnits K E
        (Units.map e.toRingEquiv.toMonoidHom z) =
      normUnits K L z
theorem

fieldNormSubgroup_eq_of_algEquiv

L41 ↗
LocalFieldTheory.DiscreteValuationField.fieldNormSubgroup_eq_of_algEquiv
Documentation

Base-field algebra-equivalent extensions have the same norm subgroup.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w
namespace LocalFieldTheory.DiscreteValuationField
variable (K : Type u) (L : Type v) (E : Type w)
variable [Field K] [Field L] [Field E]
variable [Algebra K L] [Algebra K E]
Lean source · statement
theorem fieldNormSubgroup_eq_of_algEquiv
    (e : L ≃ₐ[K] E) :
    fieldNormSubgroup K L = fieldNormSubgroup K E

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.