intCast_def — Mathlib

English

For any z ∈ ℤ, the embedded integer into MonoidAlgebra R M coincides with the basis element at the identity with coefficient z: (z : MonoidAlgebra R M) = single 1 z.

Русский

Заданное целое число z инкапсулируется в MonoidAlgebra через базис в единице: (z : MonoidAlgebra R M) = single 1 z.

LaTeX

$$$ (z : \\mathrm{MonoidAlgebra}(R,M)) = \\mathrm{single}(1 : M) (z : R). $$$

Lean4

@[to_additive (dont_translate := R)]
theorem intCast_def [MulOneClass M] (z : ℤ) : (z : MonoidAlgebra R M) = single 1 (z : R) :=
  rfl

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