det_mul_det — Mathlib

English

For bases b, b' the determinant det(b,b') is a unit whose inverse equals det(b',b).

Русский

Для базисов b, b' детерминант det(b,b') является единицей; её обратное равно det(b',b).

LaTeX

$$IsUnit (b.det b') and (b.det b')^{-1} = b'.det b$$

Lean4

theorem det_mul_det (b b' b'' : Basis ι A M) : b.det b' * b'.det b'' = b.det b'' :=
  by
  have : b'' = (b'.equiv b'' (Equiv.refl ι)).toLinearMap ∘ b' := by ext; simp
  conv_rhs => rw [this, Basis.det_comp, det_basis, mul_comm]

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