eq_or_eq_neg — Mathlib

English

For any orientation x, someBasis provides a basis whose orientation equals x.

Русский

Для любой ориентации x базис someBasis имеет ориентацию равную x.

LaTeX

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

Lean4

/-- If the index type has cardinality equal to the finite dimension, any two orientations are
equal or negations. -/
theorem eq_or_eq_neg [FiniteDimensional R M] (x₁ x₂ : Orientation R M ι) (h : Fintype.card ι = finrank R M) :
    x₁ = x₂ ∨ x₁ = -x₂ := by
  have e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm
  letI := Classical.decEq ι
  rcases e.orientation_eq_or_eq_neg x₁ with (h₁ | h₁) <;> rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂) <;>
    simp [h₁, h₂]

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