English
In a finite free algebra setting, there exists r ∈ A such that Norm_A(1 + a x) = 1 + Tr_{A/B}(x) a + r a^2, expressing a quadratic relation for near-identity perturbations.
Русский
В конечной свободной алгебре существует элемент r∈A, удовлетворяющий тождеству Norm_A(1 + a x) = 1 + Tr_{A/B}(x) a + r a^2, что описывает квадратичную аппроксимацию детерминанта.
LaTeX
$$$\\exists r \\in A: \\ \\mathrm{Norm}_A(1 + a\\cdot x) = 1 + \\mathrm{Tr}_{A/B}(x) \\cdot a + r \\cdot a^2.$$$
Lean4
theorem norm_one_add_smul {A B} [CommRing A] [CommRing B] [Algebra A B] [Module.Free A B] [Module.Finite A B] (a : A)
(x : B) : ∃ r : A, Algebra.norm A (1 + a • x) = 1 + Algebra.trace A B x * a + r * a ^ 2 := by
classical
let ι := Module.Free.ChooseBasisIndex A B
let b : Basis ι A B := Module.Free.chooseBasis _ _
haveI : Fintype ι := inferInstance
clear_value ι b
simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]
simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]
exact ⟨_, rfl⟩
