smul — Mathlib

English

If f is conformal, then c • f is also conformal for any nonzero c.

Русский

Если f конформно, то для любого ненулевого c выполняется c • f конформно.

LaTeX

$$$\\mathrm{IsConformalMap}(f) \\rightarrow \\forall c \\neq 0, \\mathrm{IsConformalMap}(c \\cdot f)$$$

Lean4

theorem smul (hf : IsConformalMap f) {c : R} (hc : c ≠ 0) : IsConformalMap (c • f) :=
  by
  rcases hf with ⟨c', hc', li, rfl⟩
  exact ⟨c * c', mul_ne_zero hc hc', li, smul_smul _ _ _⟩

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