instExpCharLinearMapSubtypeMemSubringCenterId

English

The exponential characteristic is preserved by passing to k-linear endomorphisms: if D has ExpChar p, then End_k(D) also has ExpChar p.

Русский

Экспоненциальная характеристика сохраняется при переходе к End_k(D): если D имеет ExpChar p, то End_k(D) тоже имеет ExpChar p.

LaTeX

$$$\\operatorname{ExpChar}(D) = \\operatorname{ExpChar}(\\mathrm{End}_{Z(D)}(D)).$$$

Lean4

instance {D : Type*} [DivisionRing D] {p : ℕ} [ExpChar D p] : ExpChar (D →ₗ[Subring.center D] D) p :=
  expChar_of_injective_ringHom (Algebra.lmul (Subring.center D) D).toRingHom.injective p

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