Norm and trace under scalar extension

This file records the compatibility of algebra norms and traces with scalar extension on pure tensors.

@[simp]

theorem TauCeti.Algebra.norm_baseChange_tmul {K : Type u} [CommRing K] {A : Type u_1} {B : Type u_2} [CommRing A] [Algebra K A] [Ring B] [Algebra K B] [Module.Free K B] [Module.Finite K B] (x : B) : (Algebra.norm A) (1 ⊗ₜ[K] x) = (algebraMap K A) ((Algebra.norm K) x)

Norm commutes with scalar extension on a pure tensor.

@[simp]

theorem TauCeti.Algebra.trace_baseChange_tmul {K : Type u} [CommRing K] {A : Type u_1} {B : Type u_2} [CommRing A] [Algebra K A] [CommRing B] [Algebra K B] [Module.Free K B] [Module.Finite K B] (x : B) : (Algebra.trace A (TensorProduct K A B)) (1 ⊗ₜ[K] x) = (algebraMap K A) ((Algebra.trace K B) x)

Trace commutes with scalar extension on a pure tensor.