formallyUnramified_algebraMap — Mathlib

English

(algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S

Русский

(algebraMap R S) формально незамкнуты ↔ Algebra.FormallyUnramified R S

LaTeX

$$$$ (\mathrm{algebraMap}\, R \; S).\mathrm{FormallyUnramified} \ \Longleftrightarrow \ \mathrm{Algebra.FormallyUnramified} \ R\ S. $$$$

Lean4

theorem formallyUnramified_algebraMap [Algebra R S] :
    (algebraMap R S).FormallyUnramified ↔ Algebra.FormallyUnramified R S := by
  rw [FormallyUnramified, toAlgebra_algebraMap]

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