instNoZeroSMulDivisors_2 — Mathlib

English

For the extension with K and L, the ring 𝓞K remains without zero smul divisors when viewed as a scalar module over L, i.e., NoZeroSmulDivisors(𝓞K, L).

Русский

Для расширения K⊂L кольцо целых 𝓞K рассматривается как модуль над L без нулевых смул‑делителей: NoZeroSmulDivisors(𝓞K, L).

LaTeX

$$$\\mathrm{NoZeroSmulDivisors}(\\mathcal{O}_K, L).$$$

Lean4

instance : NoZeroSMulDivisors (𝓞 K) L :=
  NoZeroSMulDivisors.trans_faithfulSMul (𝓞 K) (𝓞 L) L

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