isAlgebraic_iff — Mathlib

English

Two R-algebras related by an algebra equivalence have the same IsAlgebraic property.

Русский

Два R-алгебра, связанные алгебраическим эквивалентом, имеют одинаковую алгебраичность.

LaTeX

$$$e: A ≃ₐ[R] B \Rightarrow (\text{IsAlgebraic } R A \iff \text{IsAlgebraic } R B)$$$

Lean4

theorem isAlgebraic_iff (e : A ≃ₐ[R] B) : Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R B :=
  ⟨fun _ ↦ e.isAlgebraic, fun _ ↦ e.symm.isAlgebraic⟩

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