smulTorsor_ratio — Mathlib

English

Let c be a point of the pseudo-metric affine space P and k be a nonzero element of the field 𝕜. Then the dilation map smulTorsor by k has ratio equal to the positive norm of k, i.e. the scaling factor is ‖k‖₊.

Русский

Пусть c ∈ P и k ∈ 𝕜, k ≠ 0. Тогда дилатационная аффинная трансформация имеет отношение, равное ‖k‖₊.

LaTeX

$$$$\operatorname{ratio}(\mathrm{smulTorsor}(c, hk)) = \|k\|_{+}.$$$$

Lean4

theorem smulTorsor_ratio {c : P} {k : 𝕜} (hk : k ≠ 0) {x y : E} (h : dist x y ≠ 0) : ratio (smulTorsor c hk) = ‖k‖₊ :=
  Eq.symm <| ratio_unique_of_dist_ne_zero h <| by simp [dist_eq_norm, ← smul_sub, norm_smul]

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