Norms of binary products #
This file records the norm of an element of a product of two algebras, together with the
description of multiplication on such a product as a LinearMap.prodMap. The dependent
finite-product analogues are in TauCeti.RingTheory.NormTrace.Pi, and the trace of a binary
product is Mathlib's Algebra.trace_prod_apply.
theorem
TauCeti.Algebra.lmul_prod
{K : Type u_1}
[CommSemiring K]
{A : Type u_2}
{B : Type u_3}
[Semiring A]
[Semiring B]
[Algebra K A]
[Algebra K B]
(x : A × B)
:
Multiplication by an element of a product of two algebras acts on the two factors
independently, so as a K-linear map it is the product of the multiplications by its
components.
@[simp]
theorem
TauCeti.Algebra.norm_prod
{K : Type u_1}
[CommRing K]
{A : Type u_2}
{B : Type u_3}
[Ring A]
[Ring B]
[Algebra K A]
[Algebra K B]
[Module.Free K A]
[Module.Finite K A]
[Module.Free K B]
[Module.Finite K B]
(x : A × B)
:
The norm of an element of a product of two algebras is the product of its component norms.