polyEquivTensor' — Mathlib

English

An A-algebra isomorphism between A[X] and A ⊗R R[X], refining PolyEquivTensor.

Русский

Изоморфизм A-алгебр между A[X] и A ⊗R R[X], уточняющий PolyEquivTensor.

LaTeX

$$polyEquivTensor' : A[X] ≃ₐ[A] A ⊗[R] R[X]$$

Lean4

/-- The `A`-algebra isomorphism `A[X] ≃ₐ[A] A ⊗[R] R[X]` (when `A` is commutative). -/
def polyEquivTensor' : A[X] ≃ₐ[A] A ⊗[R] R[X]
    where
  __ := polyEquivTensor R A
  commutes' a := by simp

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