finiteType_algebraMap — Mathlib

English

Equivalence between FiniteType of the algebraMap and FiniteType of the algebra extension.

Русский

Эквивалентность между FiniteType алгебраического отображения и FiniteType расширения алгебр.

LaTeX

$$finiteType_algebraMap [Algebra A B] : (algebraMap A B).FiniteType ↔ Algebra.FiniteType A B$$

Lean4

theorem finiteType_algebraMap [Algebra A B] : (algebraMap A B).FiniteType ↔ Algebra.FiniteType A B := by
  rw [FiniteType, toAlgebra_algebraMap]

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