finitePresentation_algebraMap — Mathlib

English

The map algebraMap A B is FinitePresentation iff B is a finitely presented A-algebra.

Русский

Отображение алгебраMap A B имеет конечную презентацию тогда и только тогда, когда B — конечная презентация как A-алгебра.

LaTeX

$$$(\\text{algebraMap } A B).FinitePresentation \\iff \\text{Algebra.FinitePresentation } A B$$$

Lean4

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

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