Theorems · Theorem · field theory

PerfectRing.liftEquiv_trans

∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (g : L →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : PerfectRing M p] [inst_7 : IsPRadical i p] [inst_8 : ExpChar L p]
  [inst_9 : ExpChar N p] [inst_10 : IsPRadical g p] [inst_11 : IsPRadical (g.comp i) p],
  (PerfectRing.liftEquiv M i p).trans (PerfectRing.liftEquiv M g p) = PerfectRing.liftEquiv M (g.comp i) p

Defined in

Mathlib.FieldTheory.IsPerfectClosure

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingCommRingExpCharExpCharPerfectRingIsPRadicalExpCharExpCharIsPRadicalIsPRadical