coe_smul_closedBall — Mathlib

English

The coe map respects smul by closedBall on UnitDisk: ↑(z • w) = (z * w) in ℂ.

Русский

Соотношение вложения и умножения: ↑(z • w) = z w в ℂ для z ∈ замкнутый шар, w ∈ UnitDisk.

LaTeX

$$$ ∀ z ∈ (Metric.closedBall 0 1).Elem, w ∈ 𝔻, \\uparrow( z \\cdot w ) = (z w) $$$

Lean4

@[simp, norm_cast]
theorem coe_smul_closedBall (z : closedBall (0 : ℂ) 1) (w : 𝔻) : ↑(z • w) = (z * w : ℂ) :=
  rfl

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