The Lean 4 theorem `det_one_add_smul_hasDerivAt` in the `ChapterNavierStokesFlow` chapter of the timepiece formalization

-- Generated from ChapterNavierStokesFlow.lean — theorem BookProof.NavierStokesFlow.det_one_add_smul_hasDerivAt
import Mathlib
import Definitions.Def_ChapterNavierStokesFlow
open BookProof.NavierStokesFlow


open scoped BigOperators Matrix Kronecker ComplexOrder TensorProduct

theorem BookProof.NavierStokesFlow.det_one_add_smul_hasDerivAt (A : Matrix (Fin 3) (Fin 3) ℝ) :
    HasDerivAt (fun t : ℝ => (1 + t • A).det) A.trace 0 := by sorry