scale_eq_mul — Mathlib

English

The scale operation satisfies scale x o = (x ⊕ 1 ⊕ 0) · o, with certain cases.

Русский

Операция масштабирования выполняется согласно scale x o = (x ⊕ 1 ⊕ 0) · o, в некоторых случаях.

LaTeX

$$$\\mathrm{scale}(x,o) = (x \\ \\mathrm{oadd}\\ 1\\ 0) \\cdot o$$$

Lean4

theorem scale_eq_mul (x) [NF x] : ∀ (o) [NF o], scale x o = oadd x 1 0 * o
  | 0, _ => rfl
  | oadd e n a, h => by
    simp only [HMul.hMul]; simp only [scale]
    haveI := h.snd
    by_cases e0 : e = 0
    · simp_rw [scale_eq_mul]
      simp [Mul.mul, mul, e0, h.zero_of_zero, show x + 0 = x from repr_inj.1 (by simp)]
    · simp [e0, Mul.mul, mul, scale_eq_mul, (· * ·)]

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