centerAndRescale_radius — Mathlib

English

In the rescaled satellite configuration, the center at the last index is placed at the origin (0).

Русский

В переразмеренной спутниковой конфигурации центр последнего индекса установлен в начале координат.

LaTeX

$$$$a.centerAndRescale.c(\\text{last }N) = 0$$$$

Lean4

theorem centerAndRescale_radius {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) : a.centerAndRescale.r (last N) = 1 := by
  simp [SatelliteConfig.centerAndRescale, inv_mul_cancel₀ (a.rpos _).ne']

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