normalizedTrace_eq_of_fininteDimensional

English

If F↔K is a finite-dimensional integral extension, normalizedTrace F K equals (finrank F K)^{-1} times trace F K.

Русский

Пусть F⊂K - конечномерное интегральное расширение; нормализованный след равен (dim_F K)^{-1} на следе.

LaTeX

$$$\text{normalizedTrace } F K = (\operatorname{finrank}_F K)^{-1} \cdot \operatorname{trace}_F K$$$

Lean4

theorem normalizedTrace_eq_of_fininteDimensional [FiniteDimensional F K] :
    normalizedTrace F K = (Module.finrank F K : F)⁻¹ • trace F K :=
  LinearMap.ext <| normalizedTrace_eq_of_fininteDimensional_apply F

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