det_conj — Mathlib

English

If two linear maps f and f' agree after precomposing with a linear equivalence e, then their determinants are associated (equal up to a unit).

Русский

Если f и f' совпадают после предсопряжения линейным эквивалентом e, то их детерминанты эквивалентны (равны до умножения единицей).

LaTeX

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

Lean4

/-- Conjugating a linear equiv by a linear equiv does not change its determinant. -/
@[simp]
theorem det_conj (f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M') : LinearEquiv.det ((e.symm.trans f).trans e) = LinearEquiv.det f := by
  rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]

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