mem_center_iff — Mathlib

English

For x ∈ D, x lies in Subalgebra.center K D iff there exists a ∈ K with x = algebraMap K D a.

Русский

Для x ∈ D верно: x ∈ Subalgebra.center K D тогда и только тогда, когда существует a ∈ K such that x = algebraMap K D a.

LaTeX

$$$\\forall x:\\,D, x \\in \\operatorname{Subalgebra.center} K D \\iff \\exists a:\\,K, x = \\mathrm{algebraMap} K D\, a$$$

Lean4

theorem mem_center_iff {x : D} : x ∈ Subalgebra.center K D ↔ ∃ (a : K), x = algebraMap K D a :=
  by
  rw [center_eq_bot, Algebra.mem_bot]
  simp [eq_comm]

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