associated_det_comp_equiv — Mathlib

English

If two representations of a map differ by pre- and post- composition with equivalences, their determinants remain associated.

Русский

Если две записи отображения отличаются через пред- и пост- составление с эквивалентностями, их детерминанты остаются ассоциированными.

LaTeX

$$Associated( det(f ∘ e), det(f ∘ e') )$$

Lean4

theorem associated_det_comp_equiv {N : Type*} [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) (e e' : M ≃ₗ[R] N) :
    Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e')) :=
  by
  refine LinearMap.associated_det_of_eq_comp (e.trans e'.symm) _ _ ?_
  intro x
  simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply, LinearEquiv.apply_symm_apply]

Похожие утверждения