associated_det_of_eq_comp — Mathlib

English

For a map f: N → M and equivalences e,e': M ≃ N, the determinants det(f∘e) and det(f∘e') are associated.

Русский

Для отображения f: N → M и эквивалентностей e,e': M ≃ N детерминанты det(f∘e) и det(f∘e') ассоциированы.

LaTeX

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

Lean4

theorem associated_det_of_eq_comp (e : M ≃ₗ[R] M) (f f' : M →ₗ[R] M) (h : ∀ x, f x = f' (e x)) :
    Associated (LinearMap.det f) (LinearMap.det f') :=
  by
  suffices Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
    by
    convert this using 2
    ext x
    exact h x
  rw [← mul_one (LinearMap.det f'), LinearMap.det_comp]
  exact Associated.mul_left _ (associated_one_iff_isUnit.mpr e.isUnit_det')

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