finrank_eq_two — Mathlib

English

If S is a quadratic extension of R (IsQuadraticExtension R S), then finrank_R S = 2.

Русский

Если S является квадратичным расширением R (IsQuadraticExtension R S), то размерность S над R равна 2.

LaTeX

$$$\\operatorname{finrank} R S = 2$$$

Lean4

theorem finrank_eq_two (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S]
    [IsQuadraticExtension R S] : Module.finrank R S = 2 :=
  finrank_eq_two'

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