free_obj_coe — Mathlib

English

The underlying type of the free commutative ring on α is the multivariate polynomial ring over ℤ, i.e., (free.obj α).carrier ≅ MvPolynomial α ℤ.

Русский

Базовый тип свободного коммутативного кольца на α равен многочленам s по α над ℤ: (free.obj α).carrier ≅ MvPolynomial α ℤ.

LaTeX

$$$(\text{free.obj } \alpha).\text{carrier} = \mathrm{MvPolynomial}(\alpha, \mathbb{Z})$$$

Lean4

@[simp]
theorem free_obj_coe {α : Type u} : (free.obj α : Type u) = MvPolynomial α ℤ :=
  rfl

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