instCharPLinearMapSubtypeMemSubringCenterId

English

Let D be a division ring with center k. Then the ring of k-linear endomorphisms End_k(D) has the same characteristic as D.

Русский

Пусть D — делительная кольцо с центром k. Тогда кольцо k- линейных эндоморфизмов End_k(D) имеет ту же характеристику, что и D.

LaTeX

$$$\\operatorname{Char}(D) = \\operatorname{Char}(\\mathrm{End}_{k}(D))$$$

Lean4

/-- For a division ring `D` with center `k`, the ring of `k`-linear endomorphisms
  of `D` has the same characteristic as `D` -/
instance {D : Type*} [DivisionRing D] {p : ℕ} [CharP D p] : CharP (D →ₗ[(Subring.center D)] D) p :=
  charP_of_injective_ringHom (Algebra.lmul (Subring.center D) D).toRingHom.injective p

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