English
In a tower of finite algebras R ⊂ S ⊂ T with appropriate freeness/finite conditions, for any element x ∈ T, the trace from R to T of x equals the trace from R to S of the trace from S to T of x: Tr_{R}^{T}(x) = Tr_{R}^{S}(Tr_{S}^{T}(x)).
Русский
Пусть R ⊂ S ⊂ T — цепь конечных расширений, и выполняются нужные условия свободы/конечности. Тогда для любого x ∈ T выполняется Tr_{R}^{T}(x) = Tr_{R}^{S}(Tr_{S}^{T}(x)).
LaTeX
$$$\\operatorname{Tr}_{R}^{T} = \\operatorname{Tr}_{R}^{S} \\circ \\operatorname{Tr}_{S}^{T}$$$
Lean4
@[simp]
theorem trace_trace [Algebra S T] [IsScalarTower R S T] [Module.Free R S] [Module.Finite R S] [Module.Free S T]
[Module.Finite S T] (x : T) : trace R S (trace S T x) = trace R T x :=
trace_trace_of_basis (Module.Free.chooseBasis R S) (Module.Free.chooseBasis S T) x
