algebraMap_injective — Mathlib

English

Under NoZeroDivisors on R and a nontrivial S, any basis b of S over R ensures that the algebra map from R to S is injective.

Русский

При отсутствии нулевых делителей в R и ненулевом S отображение алгебраMap из R в S инъективно для любой базы.

LaTeX

$$$$ \text{algebraMap } R S \text{ injective} $$$$

Lean4

theorem algebraMap_injective {ι : Type*} [NoZeroDivisors R] [Nontrivial S] (b : Basis ι R S) :
    Function.Injective (algebraMap R S) :=
  have : NoZeroSMulDivisors R S := b.noZeroSMulDivisors
  FaithfulSMul.algebraMap_injective R S

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