Theorems · Theorem · field theory

IsPRadical.injective_comp_of_pNilradical_eq_bot

∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (p : ℕ) [ExpChar M p] [IsPRadical i p], pNilradical M p = ⊥ → Function.Injective fun f => f.comp i

If i : K →+* L is p-radical, then for any ring M of exponential characteristic p whose p-nilradical is zero, the map (L →+* M) → (K →+* M) induced by i is injective.

Defined in

Mathlib.FieldTheory.IsPerfectClosure

Cited by

2 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingExpCharIsPRadical