iff_algebraMap_injective — Mathlib

English

If A is a domain, NoZeroSMulDivisors R A is equivalent to the injectivity of algebraMap R A.

Русский

Если A — домен, NoZeroSMulDivisors R A эквивалентно инъективности алгебраMap R A.

LaTeX

$$$\mathrm{NoZeroSMulDivisors}\; R\; A \iff \mathrm{Injective}(\mathrm{algebraMap}\; R\; A).$$$

Lean4

theorem iff_algebraMap_injective [IsDomain A] : NoZeroSMulDivisors R A ↔ Injective (algebraMap R A) :=
  by
  rw [iff_faithfulSMul]
  exact faithfulSMul_iff_algebraMap_injective R A

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