isAlgebraic_of_not_injective — Mathlib

English

If the map algebraMap R A is not injective, then Algebra.IsAlgebraic R A holds.

Русский

Если алгебраическое отображение не инъективно, тогда A алгебраично над R.

LaTeX

$$$ \text{IsAlgebraic } R A \text{ from } \neg \text{Injective } (algebraMap R A) $$$

Lean4

theorem isAlgebraic_of_not_injective (h : ¬Function.Injective (algebraMap R A)) : Algebra.IsAlgebraic R A where
  isAlgebraic a := isAlgebraic_iff_not_injective.mpr fun inj ↦ h <| by convert inj.comp C_injective; ext; simp

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