Theorems · Theorem · field theory

IsPurelyInseparable.exists_pow_mem_range_tensorProduct

∀ {k : Type u_1} {K : Type u_2} {R : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  [inst_3 : CommRing R] [inst_4 : Algebra k R] [IsPurelyInseparable k K] (x : TensorProduct k R K),
  ∃ n > 0, x ^ n ∈ (algebraMap R (TensorProduct k R K)).range

Defined in

Mathlib.FieldTheory.PurelyInseparable.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraCommRingAlgebraIsPurelyInseparable