feat(linear_algebra/determinant): det_units_smul and `det_is_unit_s…

…mul` (#11206)

Add lemmas giving the determinant of a basis constructed with
`units_smul` or `is_unit_smul` with respect to the original basis.

src/linear_algebra/determinant.lean

@@ -511,3 +511,12 @@ begin
   { rw [basis.mk_coord_apply_ne hik, mul_zero, eq_comm],
     exact e.det.map_eq_zero_of_eq _ (by simp [hik, function.update_apply]) hik, },
 end
+
+/-- The determinant of a basis constructed by `units_smul` is the product of the given units. -/
+@[simp] lemma basis.det_units_smul (w : ι → units R) : e.det (e.units_smul w) = ∏ i, w i :=
+by simp [basis.det_apply]
+
+/-- The determinant of a basis constructed by `is_unit_smul` is the product of the given units. -/
+@[simp] lemma basis.det_is_unit_smul {w : ι → R} (hw : ∀ i, is_unit (w i)) :
+  e.det (e.is_unit_smul hw) = ∏ i, w i :=
+e.det_units_smul _