of_fact_finrank_eq_succ — Mathlib

English

If there exists a natural number n such that finrank_K V = n + 1 (as a fact), then V is finite-dimensional over K.

Русский

Если существует натуральное число n, такое что finrank_K V = n + 1 (как факт), тогда V конечномерно над K.

LaTeX

$$$\exists n \in \mathbb{N}, \; \operatorname{finrank}_K V = n + 1 \Rightarrow \operatorname{FiniteDimensional}_K V$$$

Lean4

/-- We can infer `FiniteDimensional K V` in the presence of `[Fact (finrank K V = n + 1)]`.
Use `have : FiniteDimensional K V := .of_fact_finrank_eq_succ` when needed.

This is not an instance because `n` cannot be inferred.
-/
theorem of_fact_finrank_eq_succ (n : ℕ) [hn : Fact (finrank K V = n + 1)] : FiniteDimensional K V :=
  of_finrank_eq_succ hn.out

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