instNoZeroSMulDivisorsInteger — Mathlib

English

Let R be a commutative ring and A a ring with an R-algebra structure. Let vR and vA be valuations on R and A, respectively, that extend each other via HasExtension. Then the induced pair of subrings R_int = { r ∈ R : vR(r) ≤ 1 } and A_int = { a ∈ A : vA(a) ≤ 1 } has the no zero smul divisors property: if x ∈ R_int acts nontrivially on y ∈ A_int, then x = 0 or y = 0.

Русский

Пусть R — кольцо и A — кольцо, на R действует структура алгебра над R; пусть vR и vA — valuations на R и A, расширяющиеся друг друга. Тогда у соответствующих подколец целых O(R) и O(A) выполняется свойство отсутствия нулевых смуль-дивизоров: если x ∈ O(R) действует на y ∈ O(A) так, что x·y = 0, то x = 0 или y = 0.

LaTeX

$$$\\forall x \\in v_R^{\\mathrm{integer}}, \\forall y \\in v_A^{\\mathrm{integer}},\\; (x) \\cdot y = 0 \\Rightarrow x = 0 \\lor y = 0$$$

Lean4

instance instNoZeroSMulDivisorsInteger [NoZeroSMulDivisors R A] : NoZeroSMulDivisors vR.integer vA.integer :=
  by
  refine ⟨fun {x y} e ↦ ?_⟩
  have : (x : R) • (y : A) = 0 := by simpa [Subtype.ext_iff, Algebra.smul_def] using e
  simpa only [Subtype.ext_iff, smul_eq_zero] using this

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