normalizedTrace_eq_of_fininteDimensional_apply

English

If K is finite-dimensional over F, the normalized trace equals the inverse of the dimension times the ordinary trace.

Русский

При конечной размерности K над F нормальный след равен обратной величине размерности, умноженной на обычный след.

LaTeX

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

Lean4

theorem normalizedTrace_eq_of_fininteDimensional_apply [FiniteDimensional F K] (a : K) :
    normalizedTrace F K a = (Module.finrank F K : F)⁻¹ • trace F K a :=
  normalizedTraceAux_eq_of_fininteDimensional F a

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