noZeroSMulDivisors — Mathlib

English

If R M has NoZeroSmulDivisors, then the submodule p also has NoZeroSmulDivisors with respect to the restricted action.

Русский

Если R M обладает свойством NoZeroSmulDivisors, то подмодуль p также обладает этим свойством при ограниченном действии.

LaTeX

$$[NoZeroSMulDivisors R M] → NoZeroSMulDivisors R p$$

Lean4

instance noZeroSMulDivisors [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R p :=
  ⟨fun {c} {x : p} h =>
    have : c = 0 ∨ (x : M) = 0 := eq_zero_or_eq_zero_of_smul_eq_zero (congr_arg Subtype.val h)
    this.imp_right (@Subtype.ext_iff _ _ x 0).mpr⟩

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