noZeroSMulDivisors_bot — Mathlib

English

If A has NoZeroSmulDivisors over R, then the subalgebra S, viewed as an R-algebra, also has NoZeroSmulDivisors.

Русский

Если A имеет свойство NoZeroSmulDivisors над R, то подалгебра S, рассматриваемая как R-алгебра, тоже обладает этим свойством.

LaTeX

$$$\text{NoZeroSMulDivisors}(R, S)$$$

Lean4

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

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