traceForm_toMatrix — Mathlib

English

For a local ring R with maximal ideal p and an S-algebra, the trace map commutes with the quotient by p, i.e., tracing after passage to quotients equals passing to quotients after tracing.

Русский

Для локального кольца R с максимальной идеалом p выполняется: след после взятия фактор-мода равен фактор-моду после применения следа.

LaTeX

$$$\\operatorname{trace}_{(R/p)}^{(S/pS)}(\\overline{x}) = \\overline{\\operatorname{trace}_{R}^{S}(x)}$$$

Lean4

theorem traceForm_toMatrix [DecidableEq ι] (b : Basis ι R S) (i j) :
    BilinForm.toMatrix b (traceForm R S) i j = trace R S (b i * b j) := by
  rw [BilinForm.toMatrix_apply, traceForm_apply]

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