iff_of_equiv — Mathlib

English

For any algebra isomorphism e: A ≃ₐ[R] B, FormallyUnramified R A holds if and only if FormallyUnramified R B holds.

Русский

Для любого изоморфизма A ≃ₐ[R] B имеет место эквивалентность FormallyUnramified R A ⇔ FormallyUnramified R B.

LaTeX

$$$\text{FormallyUnramified } R A \iff \text{FormallyUnramified } R B$ при наличии $e: A \simeq_A R B$$$

Lean4

theorem iff_of_equiv (e : A ≃ₐ[R] B) : FormallyUnramified R A ↔ FormallyUnramified R B :=
  ⟨fun _ ↦ of_equiv e, fun _ ↦ of_equiv e.symm⟩

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