mkPiRing — Mathlib

English

The value of mkPiRing on z and m is the product of all m_i scaled by z: (∏ i m_i) • z.

Русский

Значение mkPiRing на z и m равно произведению всех m_i, помноженному на z: (∏ i m_i) • z.

LaTeX

$$$$\bigl(\mathrm{mkPiRing}\;R\;\iota\;z\bigr)(m) = (\prod_i m_i) \cdot z.$$$$

Lean4

/-- The canonical multilinear map on `R^ι` when `ι` is finite, associating to `m` the product of
all the `m i` (multiplied by a fixed reference element `z` in the target module). See also
`mkPiAlgebra` for a more general version. -/
protected def mkPiRing [Fintype ι] (z : M₂) : MultilinearMap R (fun _ : ι => R) M₂ :=
  (MultilinearMap.mkPiAlgebra R ι R).smulRight z

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