succ_toMul — Mathlib

English

If X is a preorder with a successor order, then succ (ofAdd x) = ofAdd (succ x).

Русский

Пусть X — предпорядок с переходом к следующему; тогда succ (ofAdd x) = ofAdd (succ x).

LaTeX

$$$$\operatorname{succ}(\operatorname{Additive}.\text{ofAdd } x) = \operatorname{Additive}.\text{ofAdd } (\operatorname{succ} x)$$$$

Lean4

@[simp]
theorem succ_toMul [Preorder X] [SuccOrder X] (x : Additive X) : succ x.toMul = (succ x).toMul :=
  rfl

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