iff_of_equiv — Mathlib

English

Étale is preserved by algebra isomorphisms; FormallyEtale R A holds if and only if FormallyEtale R B holds under an isomorphism A ≃ₐ[R] B.

Русский

Étale сохраняется при алгебраических изоморфициях; FormallyEtale R A эквивалентно FormallyEtale R B при изоморфизме A ≃ₐ[R] B.

LaTeX

$$$\exists e: A \simeq_A_R B,\; \text{FormallyEtale}(R,A) \iff \text{FormallyEtale}(R,B)$$$

Lean4

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

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