instAlgebra — Mathlib

English

`R[x]/(f)` is an S-algebra; the quotient carries an algebra structure over S induced by the embedding of R into AdjoinRoot f.

Русский

`R[x]/(f)` является алгеброй над S; фактор-кольцо наследует алгебраическую структуру над S через вложение R в AdjoinRoot f.

LaTeX

$$$AdjoinRoot f \\text{ is an } S\\text{-algebra}$$$

Lean4

/-- `R[x]/(f)` is `R`-algebra -/
@[stacks 09FX "second part"]
instance [CommSemiring S] [Algebra S R] : Algebra S (AdjoinRoot f) :=
  Ideal.Quotient.algebra S

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