Module

ExtendingAbsoluteValue.lean

Nyll.ClassFieldTheory.Definitions.NormTheorems.ExtendingAbsoluteValue

1 declaration indexed from sourceView source ↗

Module documentation

This index type uses only Mathlib's absolute values and algebra map. Its elements are precisely the absolute values on L extending v on K.

Imports3

Imported by6

abbrev

ClassFieldTheory.ExtendingAbsoluteValue

Documentation

An absolute value on L whose restriction along K → L is v.

Source context 2 commands

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

namespace ClassFieldTheory
universe u v

Lean source · statement

abbrev ExtendingAbsoluteValue
    {K : Type u} [Field K] (v : AbsoluteValue K ℝ)
    (L : Type v) [Field L] [Algebra K L]