someBasis_orientation — Mathlib

English

Reiterates that someBasis provides a basis with a given orientation.

Русский

Повторно утверждается, что someBasis имеет ориентацию, равную заданной.

LaTeX

$$$$ (x.{\\rm someBasis} h).{\\rm orientation} = x $$$$

Lean4

/-- `some_basis` gives a basis with the required orientation. -/
@[simp]
theorem someBasis_orientation [Nonempty ι] [DecidableEq ι] [FiniteDimensional R M] (x : Orientation R M ι)
    (h : Fintype.card ι = finrank R M) : (x.someBasis h).orientation = x :=
  Basis.orientation_adjustToOrientation _ _

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