repr_scale — Mathlib

English

The representation of the scaled object is the product of the base representation and the scale factor: repr(scale x o) = ω^{repr x} · repr o.

Русский

Представление масштабающего объекта равно произведению представления основы на фактор масштаба: repr(scale x o) = ω^{repr x} · repr o.

LaTeX

$$$\\mathrm{repr}(\\mathrm{scale}\\ x\\ o) = \\omega^{\\mathrm{repr} x} \\cdot \\mathrm{repr}\,o$$$

Lean4

@[simp]
theorem repr_scale (x) [NF x] (o) [NF o] : repr (scale x o) = ω ^ repr x * repr o := by
  simp only [scale_eq_mul, repr_mul, repr, PNat.one_coe, Nat.cast_one, mul_one, add_zero]

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