to_isMulTorsionFree — Mathlib

English

In a Subsingleton monoid, the left-power map is injective; in particular, for any a, the map n ↦ a^n is injective.

Русский

В моноиде с подсодержанием (Subsingleton) отображение степеней слева инъективно; следовательно, для любого a последовательность n ↦ a^n инъективна.

LaTeX

$$∀ a ∈ M, injective (fun n : ℕ => a^n)$$

Lean4

@[to_additive]
instance to_isMulTorsionFree [Subsingleton M] : IsMulTorsionFree M where
  pow_left_injective _ _ := injective_of_subsingleton _

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