orientation_neg_single — Mathlib

English

Negating a single basis vector (via units_smul) negates the orientation of the basis.

Русский

Запрещает один вектор базиса с помощью единичных масштабирований — ориентация базиса меняется на противоположную.

LaTeX

$$$$ (e.{\\rm unitsSMul}(\\mathrm{update}\\,1\\,i\\,(-1))).{\\rm orientation} = -e.{\\rm orientation} $$$$

Lean4

/-- Negating a single basis vector (represented using `units_smul`) negates the corresponding
orientation. -/
@[simp]
theorem orientation_neg_single (e : Basis ι R M) (i : ι) :
    (e.unitsSMul (Function.update 1 i (-1))).orientation = -e.orientation :=
  by
  rw [orientation_unitsSMul, Finset.prod_update_of_mem (Finset.mem_univ _)]
  simp

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