NYLL
Module

NormalFieldRange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.NormalFieldRange
1 declaration indexed from sourceView source ↗

Module documentation

Ranges of embeddings of normal extensions

This file records the intrinsic image of a normal field extension inside an ambient field: every embedding over the base has the same intermediate-field range.

Imports1
  • Mathlib.FieldTheory.Normal.Basic
Imported by3

Declarations

theorem

fieldRange_eq_of_normal

L23 ↗
AlgHom.fieldRange_eq_of_normal
Documentation

Two embeddings of a normal extension into a common ambient field have the same intermediate-field range.

Source context 1 command

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

namespace AlgHom
Lean source · statement
theorem fieldRange_eq_of_normal
    {F L Ω : Type*} [Field F] [Field L] [Field Ω]
    [Algebra F L] [Algebra F Ω] [Normal F L]
    (f g : L →ₐ[F] Ω) :
    f.fieldRange = g.fieldRange

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