theorem
L29 ↗norm_one_add_eps_tmul
Algebra.norm_one_add_eps_tmul
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_one_add_eps_tmul
universe u
open scoped TensorProductLean source · statement
theorem _root_.Algebra.norm_one_add_eps_tmul
(A' B : Type u) [CommRing A'] [CommRing B] [Algebra A' B] [Module.Free A' B] [Module.Finite A'
B] (f : B) :
Algebra.norm (DualNumber A') ((1 : DualNumber A' ⊗[A'] B) + (DualNumber.eps : DualNumber A')
⊗ₜ[A'] f) =
1 + TrivSqZeroExt.inr (Algebra.trace A' B f)