negPart_algebraMap — Mathlib

English

For any real r, the negative part commutes with the algebra map: (algebraMap ℝ A r)⁻ = algebraMap ℝ A r⁻.

Русский

Для любого вещественного r отрицательная часть сохраняется под отображением алгебра map: (algebraMap ℝ A r)⁻ = algebraMap ℝ A r⁻.

LaTeX

$$$( \\operatorname{algebraMap}_{\mathbb{R}} A \\; r)^- = \\operatorname{algebraMap}_{\mathbb{R}} A \\; r^-$$$

Lean4

@[simp]
theorem negPart_algebraMap (r : ℝ) : (algebraMap ℝ A r)⁻ = algebraMap ℝ A r⁻ :=
  by
  rw [CFC.negPart_def, cfcₙ_eq_cfc]
  simp

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