finrank_eq_two — Mathlib

English

If R has StrongRankCondition, then the finite rank of QuadraticAlgebra R a b is 2.

Русский

Пусть R удовлетворяет условию StrongRankCondition; тогда модульная конечная размерность QuadraticAlgebra R a b равна 2.

LaTeX

$$$\operatorname{finrank}_R\bigl(\QuadraticAlgebra R a b\bigr) = 2$$$

Lean4

theorem finrank_eq_two [StrongRankCondition R] : Module.finrank R (QuadraticAlgebra R a b) = 2 := by
  simp [Module.finrank, rank_eq_two]

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