rank_eq_two — Mathlib

English

If R satisfies StrongRankCondition, then QuadraticAlgebra R a b is a free module of rank 2 over R.

Русский

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

LaTeX

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

Lean4

theorem rank_eq_two [StrongRankCondition R] : Module.rank R (QuadraticAlgebra R a b) = 2 := by
  simp [rank_eq_card_basis (basis a b)]

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