isSeparable_iff — Mathlib

English

IsSeparable is preserved under an algebra equivalence between two algebras over F.

Русский

Разделяемость сохраняется под алгебраическим эквивалентом между двумя алгебрами над F.

LaTeX

$$IsSeparable F K ↔ IsSeparable F E under e : K ≃ₐ[F] E$$

Lean4

/-- Transfer `IsSeparable` across an `AlgEquiv`. -/
theorem isSeparable_iff {x : K} : IsSeparable F (e x) ↔ IsSeparable F x := by
  simp only [IsSeparable, minpoly.algEquiv_eq e x]

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