Algebra.norm_one_tmul_eq_algebraMap_norm
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_one_tmul_eq_algebraMap_norm
universe u v w
open scoped TensorProductLean source · statement
theorem _root_.Algebra.norm_one_tmul_eq_algebraMap_norm
{K : Type u} [CommRing K] {L : Type v} [Ring L] [Algebra K L] [Module.Free K L] [Module.Finite
K L]
(K' : Type w) [CommRing K'] [Algebra K K'] (x : L) :
Algebra.norm K' ((1 : K') ⊗ₜ[K] x : K' ⊗[K] L) = algebraMap K K' (Algebra.norm K x)