Theorems · Theorem · field theory

IsPerfectClosure.equiv_comp_equiv_apply

∀ {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) (j : K →+* M) (k : K →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : ExpChar L p] [inst_7 : PerfectRing L p] [inst_8 : IsPerfectClosure i p]
  [inst_9 : PerfectRing M p] [inst_10 : IsPerfectClosure j p] [inst_11 : ExpChar N p] [inst_12 : PerfectRing N p]
  [inst_13 : IsPerfectClosure k p] (x : L),
  (IsPerfectClosure.equiv j k p) ((IsPerfectClosure.equiv i j p) x) = (IsPerfectClosure.equiv i k p) x

Defined in

Mathlib.FieldTheory.IsPerfectClosure

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingCommRingExpCharExpCharExpCharPerfectRingIsPerfectClosurePerfectRingIsPerfectClosureExpCharPerfectRingIsPerfectClosure