algebra — Mathlib

English

If A is an R-algebra, then A[X] carries an R[X]-algebra structure extending that on A; hence there is a natural algebra structure on A[X] over R[X].

Русский

Если A — R-алгебра, то A[X] имеет структуру R[X]-алгебры, наследующуюся от A.

LaTeX

$$$A[X]\text{ is an } R[X]\text{-algebra.}$$$

Lean4

/-- If `A` is an `R`-algebra, then `A[X]` is an `R[X]` algebra.
This gives a diamond for `Algebra R[X] R[X][X]`, so this is not a global instance. -/
@[reducible]
def algebra : Algebra R[X] A[X] :=
  (mapRingHom (algebraMap R A)).toAlgebra' fun _ _ ↦ by ext;
    rw [coeff_mul, ← Finset.Nat.sum_antidiagonal_swap, coeff_mul]; simp [Algebra.commutes]

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