mulSingle_injective — Mathlib

English

For a fixed i, the map x ↦ mulSingle i x is injective from M_i into the product space ∀ i, M i.

Русский

Для фиксированного i отображение x ↦ mulSingle i x однозначно инъективно из M_i в пространство функций ∀ i, M_i.

LaTeX

$$$\text{Injective}(\mathrm{mulSingle}\ i)\;:\; M i \to \:\forall k, M k$$$

Lean4

@[to_additive]
theorem mulSingle_injective (i : ι) : Function.Injective (mulSingle i : M i → ∀ i, M i) :=
  Function.update_injective _ i

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