noZeroSMulDivisors_bot — Mathlib

English

If the ambient module A over R has NoZeroSmulDivisors, then the subalgebra S over R also has NoZeroSmulDivisors: if c ∈ R and x ∈ S satisfy c x = 0 in A, then either c = 0 or x = 0 in S.

Русский

Если у модуля A над R есть свойство NoZeroSmulDivisors, то у подпалгебры S над R тоже есть это свойство: если c ∈ R и x ∈ S удовлетворяют c x = 0 в A, то либо c = 0, либо x = 0 в S.

LaTeX

$$$ \\forall c \\in R,\\ \\forall x \\in S:\\ c\\cdot x = 0_A \\Rightarrow c = 0 \\lor x = 0_S. $$$

Lean4

instance noZeroSMulDivisors_bot [NoZeroSMulDivisors R A] : NoZeroSMulDivisors R S :=
  ⟨fun {c x} h =>
    have : c = 0 ∨ (x : A) = 0 := eq_zero_or_eq_zero_of_smul_eq_zero (congr_arg ((↑) : S → A) h)
    this.imp_right Subtype.ext⟩

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