equivSignedMeasureₗ — Mathlib

English

The complex measures form a linear equivalence to SignedMeasure α × SignedMeasure α, compatible with scalar multiplication from a ring R.

Русский

Комплексные меры образуют линейную эквивалентность к паре смешанных мер, сохраняющую масштабирование из кольца R.

LaTeX

$$equivSignedMeasureₗ : ComplexMeasure α ≃ₗ[R] SignedMeasure α × SignedMeasure α$$

Lean4

/-- The complex measures form a linear isomorphism to the type of pairs of signed measures. -/
@[simps]
def equivSignedMeasureₗ : ComplexMeasure α ≃ₗ[R] SignedMeasure α × SignedMeasure α :=
  { equivSignedMeasure with
    map_add' := fun c d => by rfl
    map_smul' := by
      intro r c
      dsimp
      ext
      · simp [Complex.smul_re]
      · simp [Complex.smul_im] }

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