C_inv — Mathlib

English

For any scalar r in k, the inverse of the constant multivariate power series C r is C(r^{-1}); when r = 0, the convention is compatible with 0⁻¹ = 0.

Русский

Для любого скаляра r в k обратное константного ряда C r является C(r⁻¹); если r = 0, то используется соглашение 0⁻¹ = 0.

LaTeX

$$$ (C(\sigma:=\sigma)\; r)^{-1} = C\; r^{-1} $ for all r \in k$$

Lean4

@[simp]
theorem C_inv (r : k) : (C (σ := σ) r)⁻¹ = C r⁻¹ :=
  by
  rcases eq_or_ne r 0 with (rfl | hr)
  · simp
  rw [MvPowerSeries.inv_eq_iff_mul_eq_one, ← map_mul, inv_mul_cancel₀ hr, map_one]
  simpa using hr

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