isPurelyInseparable_iff — Mathlib

English

Purely inseparable property is invariant under F-algebra isomorphisms: for any e: K ≃_F E, IsPurelyInseparable F K holds if and only if IsPurelyInseparable F E holds.

Русский

Свойство чистой безразделимости инвариантно при F-алгебраических изоморфиях: для любого e: K ≃_F E выполняется IsPurelyInseparable F K ↔ IsPurelyInseparable F E.

LaTeX

$$$ \forall F,E,K\,[\text{CommRing } F] [\text{Ring } E] [\text{Algebra } F E] {\?} (e: K \cong_F E),\ IsPurelyInseparable(F,K) \iff IsPurelyInseparable(F,E). $$$

Lean4

theorem isPurelyInseparable_iff (e : K ≃ₐ[F] E) : IsPurelyInseparable F K ↔ IsPurelyInseparable F E :=
  ⟨fun _ ↦ e.isPurelyInseparable, fun _ ↦ e.symm.isPurelyInseparable⟩

Похожие утверждения