oriented — Mathlib

English

Every module is canonically oriented when the index set is empty.

Русский

Каждый модуль имеет каноническую ориентацию при пустом индексе.

LaTeX

$$$\text{IsEmpty.oriented}: \text{instance oriented for IsEmpty ι}$$$

Lean4

/-- A module is canonically oriented with respect to an empty index type. -/
instance (priority := 100) oriented [IsEmpty ι] : Module.Oriented R M ι where
  positiveOrientation :=
    rayOfNeZero R (AlternatingMap.constLinearEquivOfIsEmpty 1) <|
      AlternatingMap.constLinearEquivOfIsEmpty.injective.ne (by exact one_ne_zero)

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