Module

BaseChangeNormTrace.lean

Nyll.ValuedFieldTheory.Valuation.Completion.BaseChangeNormTrace

2 declarations indexed from sourceView source ↗

Module documentation

Norm and trace under scalar extension

Norm and trace formulas compare multiplication by an element of L before and after extending scalars from K to K_v. These lemmas state that comparison directly for the canonical element 1 ⊗ₜ x.

Imports5

Mathlib.LinearAlgebra.Charpoly.BaseChange
Mathlib.LinearAlgebra.Trace
Mathlib.RingTheory.Norm.Basic
Mathlib.RingTheory.Trace.Basic
Mathlib.RingTheory.TensorProduct.Basic

Imported by2

theorem

algebra_norm_baseChange_tmul

L33 ↗

ValuationTheory.Completion.algebra_norm_baseChange_tmul

Documentation

Algebra norm commutes with scalar extension.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory
namespace Completion
universe u v w
open scoped TensorProduct

Lean source · statement

theorem algebra_norm_baseChange_tmul
    {K A L : Type*} [Field K] [Field A] [CommRing L]
    [Algebra K A] [Algebra K L]
    [Module.Free K L] [Module.Finite K L]
    (x : L) :
    Algebra.norm A (1 ⊗ₜ[K] x : A ⊗[K] L) =
      algebraMap K A (Algebra.norm K x)

theorem

algebra_trace_baseChange_tmul

L44 ↗

ValuationTheory.Completion.algebra_trace_baseChange_tmul