finite_algebraMap — Mathlib

English

For an algebra structure A → B, the map algebraMap A B is finite iff B is a finitely generated A-module.

Русский

Пусть есть структура алгебры A → B; отображение algebraMap A B конечно порождает B как A-модуль.

LaTeX

$$algebraMap A B.Finite ↔ Module.Finite A B$$

Lean4

@[simp]
theorem finite_algebraMap [Algebra A B] : (algebraMap A B).Finite ↔ Module.Finite A B := by
  rw [RingHom.Finite, toAlgebra_algebraMap]

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