noZeroDivisors — Mathlib

English

If A has no zero divisors and S is a subalgebra of A, then S has no zero divisors as a subring.

Русский

Если A не имеет нулевых делителей, и S — подалгебра A, то S как подкольцо также не имеет нулевых делителей.

LaTeX

$$$\text{NoZeroDivisors}(A) \Rightarrow \text{NoZeroDivisors}(S)$$$

Lean4

instance noZeroDivisors {R A : Type*} [CommSemiring R] [Semiring A] [NoZeroDivisors A] [Algebra R A]
    (S : Subalgebra R A) : NoZeroDivisors S :=
  inferInstanceAs (NoZeroDivisors S.toSubsemiring)

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