isUnit — Mathlib

English

If v is a nonzero vector in a finite-dimensional space over K, the span of {v} has dimension 1.

Русский

Пусть v — ненулевой вектор в конечномерном пространстве над K; линspan{v} имеет размерность 1.

LaTeX

$$$v \neq 0 \Rightarrow \operatorname{finrank}_K(\operatorname{Span} \{v\}) = 1$$$

Lean4

theorem isUnit (F : Type*) {K : Type*} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K] {x : K}
    (H : x ≠ 0) : IsUnit x :=
  let _ := divisionRingOfFiniteDimensional F K;
  H.isUnit

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