mulSingle_eq_of_ne' — Mathlib

English

Let i ≠ i'. For any x in M_i, the value of the updated function at i' is 1, i.e. mulSingle i x i' = 1 when i ≠ i'.

Русский

Пусть i ≠ i'. Пусть x ∈ M_i. Значение обновленной функции в индексе i' равно 1, то есть mulSingle i x i' = 1 при i ≠ i'.

LaTeX

$$$\forall {i i' : ι} (h : i' \neq i) (x : M i),\; mulSingle i x i' = 1$$$

Lean4

/-- Abbreviation for `mulSingle_eq_of_ne h.symm`, for ease of use by `simp`. -/
@[to_additive (attr := simp) /-- Abbreviation for `single_eq_of_ne h.symm`, for ease of use by `simp`. -/
    ]
theorem mulSingle_eq_of_ne' {i i' : ι} (h : i ≠ i') (x : M i) : mulSingle i x i' = 1 :=
  mulSingle_eq_of_ne h.symm x

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