relrank_eq_rank_of_le — Mathlib

English

If A ≤ B, then relrank A B = Module.rank A (extendScalars h).

Русский

Если A ⊆ B, то relrank A B = Module.rank A (extendScalars h).

LaTeX

$$$A \\le B \\Rightarrow \\mathrm{relrank}(A,B) = \\mathrm{Module.rank}\\,A\\,(\\mathrm{extendScalars}\\,h)$$$

Lean4

/-- If `A ≤ B`, then `Subfield.relrank A B` is `[B : A]`. -/
theorem relrank_eq_rank_of_le (h : A ≤ B) : relrank A B = Module.rank A (extendScalars h) :=
  by
  rw [relrank]
  have := inf_of_le_left h
  congr!

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