Relation between Norms and Traces

theorem Algebra.norm_one_add_smul {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [Module.Free A B] [Module.Finite A B] (a : A) (x : B) : ∃ (r : A), (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2