union_zero — Mathlib

English

The union of the character space with {0} equals the set of all φ satisfying φ(xy)=φ(x)φ(y).

Русский

Объединение пространства характеристик и {0} является множеством всех функционалов φ, удовлетворяющих φ(xy)=φ(x)φ(y).

LaTeX

$$$\\text{characterSpace } 𝕜 A \\cup \\{0\\} = \\{φ : WeakDual 𝕜 A ∣ ∀ x,y, φ(xy)=φ(x)φ(y)\\}$$$

Lean4

theorem union_zero : characterSpace 𝕜 A ∪ {0} = {φ : WeakDual 𝕜 A | ∀ x y : A, φ (x * y) = φ x * φ y} :=
  le_antisymm
    (by
      rintro φ (hφ | rfl)
      · exact hφ.2
      · exact fun _ _ => by exact (zero_mul (0 : 𝕜)).symm)
    fun φ hφ => Or.elim (em <| φ = 0) Or.inr fun h₀ => Or.inl ⟨h₀, hφ⟩

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