inf_relfinrank_left — Mathlib

English

Let A and B be intermediate fields of E over F. Then the relative finite rank of A ∩ B over A equals the relative finite rank of B over A.

Русский

Пусть A и B — промежуточные поля E над F. Тогда относительная конечная размерность (A ∩ B) над A равна относительной конечной размерности B над A.

LaTeX

$$$\operatorname{relfinrank}(A \cap B, A) = \operatorname{relfinrank}(B, A)$$$

Lean4

theorem inf_relfinrank_left : relfinrank (A ⊓ B) A = relfinrank B A :=
  congr(toNat $(inf_relrank_left A B))

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