instNoZeroSMulDivisors — Mathlib

English

The extension 𝓞_K over K has the NoZeroSmulDivisors property: if a ≠ 0 in 𝓞_K and b ∈ K, then ab ≠ 0.

Русский

Расширение 𝓞_K над K имеет свойство NoZeroSmulDivisors: при a ≠ 0 в 𝓞_K и b ∈ K, произведение ab не равно 0.

LaTeX

$$$\forall a \in \mathcal{O}_K, a \neq 0 \Rightarrow (\forall b \in K, ab \neq 0).$$$

Lean4

instance : NoZeroSMulDivisors (𝓞 K) K :=
  inferInstanceAs (NoZeroSMulDivisors (integralClosure _ _) _)

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