relrank_mul_relrank — Mathlib

English

If A ≤ B ≤ C are intermediate F-subfields of E, then relrank A B · relrank B C = relrank A C.

Русский

Если A ≤ B ≤ C — промежуточные поля над F в E, то relrank A B · relrank B C = relrank A C.

LaTeX

$$$ A \le B \le C \Rightarrow \operatorname{relrank} A B \cdot \operatorname{relrank} B C = \operatorname{relrank} A C $$$

Lean4

theorem relrank_mul_relrank (h1 : A ≤ B) (h2 : B ≤ C) : relrank A B * relrank B C = relrank A C :=
  Subfield.relrank_mul_relrank h1 h2

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