right — Mathlib

English

In a tower F ⊆ K ⊆ A, if A is finite over F, then A is finite over K.

Русский

В башне F ⊆ K ⊆ A, если A конечно над F, то A конечно над K.

LaTeX

$$$\\text{Module.Finite } F A \\Rightarrow \\text{Module.Finite } K A$$$

Lean4

@[stacks 09G5]
theorem right [hf : Module.Finite F A] : Module.Finite K A :=
  let ⟨⟨b, hb⟩⟩ := hf
  ⟨⟨b,
      Submodule.restrictScalars_injective F _ _ <|
        by
        rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]
        exact Submodule.subset_span⟩⟩

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