of_mem_adjoin_singleton — Mathlib

English

If a lies in the subalgebra generated by f, then a is semisimple.

Русский

Если a лежит в подалгебре, порождаемой f, то a семисемпсим.

LaTeX

$$$ a \in \mathrm{algebra\ adjoin}_K(\{f\}) \Rightarrow IsSemisimple(a)$$$

Lean4

theorem of_mem_adjoin_singleton {a : End K M} (ha : a ∈ Algebra.adjoin K { f }) : a.IsSemisimple := by
  rw [Algebra.adjoin_singleton_eq_range_aeval] at ha; obtain ⟨p, rfl⟩ := ha; exact .aeval hf _

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