noZeroDivisors — Mathlib

English

If A has no zero divisors and S ≤ A is a nonunital subalgebra, then S has no zero divisors as a subalgebra.

Русский

Если A не имеет делителей нуля и S ⊆ A — немонолитная подалгебра, то S также не имеет делителей нуля как подалгебра.

LaTeX

$$$\\forall a,b \\in S,\\ ab=0 \\Rightarrow a=0 \\text{ or } b=0$$$

Lean4

instance noZeroDivisors {R A : Type*} [CommSemiring R] [NonUnitalSemiring A] [NoZeroDivisors A] [Module R A]
    (S : NonUnitalSubalgebra R A) : NoZeroDivisors S :=
  NonUnitalSubsemiringClass.noZeroDivisors S

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