map_intNormAux — Mathlib

English

There is a compatibility between intTrace and the algebra map when embedding A into K and B into L, matching trace values through the isomorphism of integral closures.

Русский

Существуют совместимости между intTrace и отображениями по базам через изоморфизм интегральных замкнений, согласующие значения следа.

LaTeX

$$$[IsIntegrallyClosed A]\\ [IsIntegrallyClosed B] \\Rightarrow algebraMap A K (Algebra.intTrace A B x) = Algebra.trace K L (algebraMap B L x)$$$

Lean4

theorem map_intNormAux (x : B) : algebraMap A K (Algebra.intNormAux A K L B x) = Algebra.norm K (algebraMap B L x) :=
  by
  dsimp [Algebra.intNormAux]
  exact IsIntegralClosure.algebraMap_mk' _ _ _

Похожие утверждения