Module

Extension.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.Extension

1 declaration indexed from sourceView source ↗

Module documentation

Extensions of absolute values

A reusable predicate for exact extension along an algebra map.

Imports3

Mathlib.Algebra.Algebra.Basic
Mathlib.Basic.Real.Basic
Mathlib.Topology.UniformSpace.AbsoluteValue

Imported by7

def

Extends

AbsoluteValue.Extends

Documentation

The target absolute value agrees with the base absolute value along the algebra map.

Source context 1 command

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

namespace AbsoluteValue

Lean source · statement

def Extends {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) : Prop