posPart_algebraMap — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem posPart_algebraMap (r : ℝ) : (algebraMap ℝ A r)⁺ = algebraMap ℝ A r⁺ :=
  by
  rw [CFC.posPart_def, cfcₙ_eq_cfc]
  simp

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