instNoZeroDivisors — Mathlib

English

If A has no zero divisors, then any nonunital star-subalgebra S inherits NoZeroDivisors.

Русский

Если у A нет нулевых делителей, то любая неединичная звёздная подпалгебра S наследует свойство отсутствия нулевых делителей.

LaTeX

$$NoZeroDivisors(S).$$

Lean4

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

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