mulHead — Mathlib

English

The head of replaceHead equals the replacement element x, i.e., (replaceHead x h w).head = x.

Русский

Голова replaceHead равна замещающему элементу x: (replaceHead x h w).head = x.

LaTeX

$$$$\\text{head}(\\text{replaceHead}(x,h,w)) = x.$$$$

Lean4

/-- One can multiply an element from the left to a non-empty reduced word if it does not cancel
with the first element in the word. -/
def mulHead {i j : ι} (w : NeWord M i j) (x : M i) (hnotone : x * w.head ≠ 1) : NeWord M i j :=
  replaceHead (x * w.head) hnotone w

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