instNoZeroSMulDivisors_1 — Mathlib

English

If the algebra map from K to L is injective, then the ring of integers 𝓞K has the no zero smul divisors property with respect to 𝓞L; equivalently, the action of 𝓞K on 𝓞L has no nontrivial zero divisors.

Русский

Если алгебраическая карта из K в L инъективна, то у кольца целых 𝓞K по отношению к 𝓞L отсутствуют нулевые смул‑делители; иначе говоря, действие 𝓞K на 𝓞L не имеет ненулевых нулевых делителей.

LaTeX

$$$\\text{NoZeroSmulDivisors}(\\mathcal{O}_K, \\mathcal{O}_L),$\n\\quad \\text{(when the algebra map }K\\to L\\text{ is injective).}$$$

Lean4

instance : NoZeroSMulDivisors (𝓞 K) (𝓞 L) :=
  NoZeroSMulDivisors.iff_algebraMap_injective.mpr <| algebraMap.injective K L

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