negPart_mul_posPart — Mathlib

English

This confirms the PosPart operator is defined as a structure on A via the specified functional calculus.

Русский

Подтверждается, что оператор PosPart определён как структура на A через заданный функциональный калькулятор.

LaTeX

$$Not applicable$$

Lean4

@[simp]
theorem negPart_mul_posPart (a : A) : a⁻ * a⁺ = 0 :=
  by
  rw [posPart_def, negPart_def]
  by_cases ha : IsSelfAdjoint a
  · rw [← cfcₙ_mul _ _, ← cfcₙ_zero ℝ a]
    refine cfcₙ_congr (fun x _ ↦ ?_)
    simp only [_root_.posPart_def, _root_.negPart_def]
    simpa using le_total 0 x
  · simp [cfcₙ_apply_of_not_predicate a ha]

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