iff_of_equiv — Mathlib

English

If A and B are algebras over R and there is an R-algebra isomorphism e : A ≃ₐ[R] B, then A is formally smooth over R if and only if B is formally smooth over R.

Русский

Если A и B являются алгебрами над R и существует изоморфизм R-алгебр e: A ≃ₐ[R] B, то A формально гладко над R тогда и только тогда, когда B формально гладко над R.

LaTeX

$$$\operatorname{FormallySmooth}(R,A) \iff \operatorname{FormallySmooth}(R,B)$$$

Lean4

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

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