English
If b is a basis and e is a bijection between index sets, then det after reindexing with e.symm and compensating with e on the inputs returns the original determinant.
Русский
Если есть базис b и биекция между наборами индексов, то перестановка на обратную сторону восстанавливает исходный детерминант.
LaTeX
$$(b.reindex e.symm).det (v ∘ e) = b.det v$$
Lean4
/-- If we fix a background basis `e`, then for any other basis `v`, we can characterise the
coordinates provided by `v` in terms of determinants relative to `e`. -/
theorem det_smul_mk_coord_eq_det_update {v : ι → M} (hli : LinearIndependent R v) (hsp : ⊤ ≤ span R (range v)) (i : ι) :
e.det v • (Basis.mk hli hsp).coord i = e.det.toMultilinearMap.toLinearMap v i :=
by
apply (Basis.mk hli hsp).ext
intro k
rcases eq_or_ne k i with (rfl | hik) <;>
simp only [Algebra.id.smul_eq_mul, coe_mk, LinearMap.smul_apply, MultilinearMap.toLinearMap_apply]
· rw [mk_coord_apply_eq, mul_one, update_eq_self]
congr
· rw [mk_coord_apply_ne hik, mul_zero, eq_comm]
exact e.det.map_eq_zero_of_eq _ (by simp [hik]) hik
