quotient — Mathlib

English

If A has a finite presentation, then the base-changed algebra B ⊗_R A has a finite presentation over B.

Русский

Базовое изменение B ⊗_R A имеет конечную презентацию над B, если A имеет конечную презентацию.

LaTeX

$$$\\text{Algebra.FinitePresentation } R A \\Rightarrow \\text{Algebra.FinitePresentation } B (B\\otimes_R A)$$$

Lean4

instance quotient (R : Type*) {S : Type*} [CommSemiring R] [CommRing S] [Algebra R S] (I : Ideal S)
    [h : Algebra.FiniteType R S] : Algebra.FiniteType R (S ⧸ I) :=
  Algebra.FiniteType.trans h inferInstance

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