algebraBase_injective — Mathlib

English

The algebra map from A to CyclotomicRing is injective under NoZeroSmulDivisors hypotheses.

Русский

Алгебраическое отображение из A в CyclotomicRing инъективно при условиях NoZeroSmulDivisors.

LaTeX

$$$\\text{algebraMap}: A \\to CyclotomicRing(n,A,K)\\text{ injective}$$$

Lean4

theorem algebraBase_injective [IsFractionRing A K] : Function.Injective <| algebraMap A (CyclotomicRing n A K) :=
  FaithfulSMul.algebraMap_injective _ _

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