finite_sup — Mathlib

English

If E1 and E2 are subalgebras of a common algebra and both are finite over the same base, then their join E1 ⊔ E2 is finite over the base.

Русский

Если E1 и E2 — подалгебры одного кольца и обе конечны над базовым кольцом, то их суммарное объединение E1 ⊔ E2 также конечно над базисом.

LaTeX

$$$\text{Module.Finite} K ↥(E_1 ⊔ E_2)$$$

Lean4

theorem finite_sup {K L : Type*} [CommSemiring K] [CommSemiring L] [Algebra K L] (E1 E2 : Subalgebra K L)
    [Module.Finite K E1] [Module.Finite K E2] : Module.Finite K ↥(E1 ⊔ E2) :=
  by
  rw [← E1.range_val, ← E2.range_val, ← Algebra.TensorProduct.productMap_range]
  exact Module.Finite.range (Algebra.TensorProduct.productMap E1.val E2.val).toLinearMap

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