Theorems · Theorem · field theory

IsPRadical.injective_comp

∀ {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] [IsReduced M], Function.Injective fun f => f.comp i

If i : K →+* L is p-radical, then for any reduced ring M of exponential characteristic p, the map (L →+* M) → (K →+* M) induced by i is injective. A special case of IsPRadical.injective_comp_of_pNilradical_eq_bot and a generalization of IsPurelyInseparable.injective_comp_algebraMap.

Defined in

Mathlib.FieldTheory.IsPerfectClosure

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingExpCharIsPRadicalIsReduced