transfer_normal — Mathlib

English

If f: E ≃ₐ[F] E' is an algebra equivalence and E is normal over F, then E' is normal over F, and conversely.

Русский

Если есть алгебраическое тождество f: E ≃ₐ[F] E' и E нормально над F, то E' нормально над F, и наоборот.

LaTeX

$$$\mathrm{Normal} F E \iff \mathrm{Normal} F E'$ for $f: E \simeq_{F} E'$$$

Lean4

theorem transfer_normal (f : E ≃ₐ[F] E') : Normal F E ↔ Normal F E' :=
  ⟨fun _ ↦ Normal.of_algEquiv f, fun _ ↦ Normal.of_algEquiv f.symm⟩

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