isSeparable_residueField_iff — Mathlib

English

Under maximal p and q, Algebra.IsSeparable p.ResidueField q.ResidueField iff Algebra.IsSeparable (A ⧸ p) (B ⧸ q).

Русский

При максимальных p и q разделимость p.ResidueField ⊂ q.ResidueField эквивалентна разделимости (A ⧸ p) ⧸ (B ⧸ q).

LaTeX

$$$\mathrm{Algebra.IsSeparable}(p.\mathrmResidueField, q.\mathrmResidueField) \iff \mathrm{Algebra.IsSeparable}(A/ p, B/ q)$$$

Lean4

theorem isSeparable_residueField_iff [p.IsMaximal] [q.IsMaximal] :
    Algebra.IsSeparable p.ResidueField q.ResidueField ↔ Algebra.IsSeparable (A ⧸ p) (B ⧸ q) :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

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