mem_center_iff — Mathlib

English

The integer cast into CentroidHom α corresponds to the endomorphism a ↦ z a, matching the scalar action of integers.

Русский

Целочисленное приведение в CentroidHom α соответствует эндоморфизмy a ↦ z a, совпадающему со скалярным действием целых чисел.

LaTeX

$$$\forall z ∈ \mathbb{Z}, (z : CentroidHom(\alpha)) (a) = z a$$$

Lean4

theorem _root_.NonUnitalNonAssocCommSemiring.mem_center_iff (a : α) :
    a ∈ NonUnitalSubsemiring.center α ↔ ∀ b : α, Commute (L b) (L a) :=
  by
  rw [NonUnitalNonAssocSemiring.mem_center_iff, CentroidHom.centroid_eq_centralizer_mulLeftRight,
    Subsemiring.mem_centralizer_iff, AddMonoid.End.mulRight_eq_mulLeft, Set.union_self]
  aesop

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