smul_inv — Mathlib

English

For any scalar r in k and any multivariate power series φ, we have (r • φ)⁻¹ = r⁻¹ • φ⁻¹.

Русский

Для любого скаляра r в k и любого ряда φ выполняется (r • φ)⁻¹ = r⁻¹ • φ⁻¹.

LaTeX

$$$\forall r \in k, \forall \phi \in \mathrm{MvPowerSeries}(\sigma,k), (r \cdot \phi)^{-1} = r^{-1} \cdot \phi^{-1}$$$

Lean4

@[simp]
theorem smul_inv (r : k) (φ : MvPowerSeries σ k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹ := by simp [smul_eq_C_mul, mul_comm]

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