polyEquivTensor — Mathlib

English

The construct PolyEquivTensor provides an R-algebra equivalence between A[X] and A ⊗R R[X], built from toFunAlgHom and invFun.

Русский

Конструкция PolyEquivTensor обеспечивает R-алгебраическое эквивиалент между A[X] и A ⊗R R[X], построенное на toFunAlgHom и invFun.

LaTeX

$$PolyEquivTensor R A : A[X] ≃ₐ[R] A ⊗[R] R[X]$$

Lean4

/-- The `R`-algebra isomorphism `A[X] ≃ₐ[R] (A ⊗[R] R[X])`.
-/
def polyEquivTensor : A[X] ≃ₐ[R] A ⊗[R] R[X] :=
  AlgEquiv.symm { PolyEquivTensor.toFunAlgHom R A, PolyEquivTensor.equiv R A with }

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