expChar_of_injective_algebraMap — Mathlib

English

If the algebra map R →+* A is injective, then ExpChar R p holds if ExpChar A p holds.

Русский

Если отображение R →+* A инъективно, то ExpChar R p выполняется при ExpChar A p.

LaTeX

$$$( \\operatorname{algebraMap} R A ) \\text{ injective } \\Rightarrow ( \\operatorname{ExpChar}(R,p) \\iff \\operatorname{ExpChar}(A,p) )$$$

Lean4

/-- If the algebra map `R →+* A` is injective then `A` has the same exponential characteristic
as `R`. -/
theorem expChar_of_injective_algebraMap {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (h : Function.Injective (algebraMap R A)) (q : ℕ) [ExpChar R q] : ExpChar A q :=
  expChar_of_injective_ringHom h q

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