pow_right_injective_iff_pow_injective

English

The map m ↦ n^m is injective if and only if the map pow n is injective; i.e., injectivity of the exponentiation map to powers corresponds to injectivity of the Submonoid.pow operation.

Русский

Степень m ↦ n^m инъективна тогда и только тогда, когда отображение pow n инъективно; то есть инъективность экспоненциации соответствует инъективности Submonoid.pow.

LaTeX

$$$ (\\operatorname{Injective}(\\lambda m: \\mathbb{N}, n^m)) \\iff (\\operatorname{Injective}(\\text{pow } n)) $$$

Lean4

theorem pow_right_injective_iff_pow_injective {n : M} :
    (Function.Injective fun m : ℕ => n ^ m) ↔ Function.Injective (pow n) :=
  Subtype.coe_injective.of_comp_iff (pow n)

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