noZeroSMulDivisors_top — Mathlib

English

If A has no zero divisors, then the natural scalar action of the subalgebra S on A also has no zero smul divisors: if c ∈ S and x ∈ A satisfy c·x = 0, then c = 0 or x = 0.

Русский

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

LaTeX

$$$\forall c \in S,\; \forall x \in A,\; c x = 0 \Rightarrow c = 0 \text{ or } x = 0$$$

Lean4

instance noZeroSMulDivisors_top [NoZeroDivisors A] (S : Subalgebra R A) : NoZeroSMulDivisors S A :=
  ⟨fun {c} x h =>
    have : (c : A) = 0 ∨ x = 0 := eq_zero_or_eq_zero_of_mul_eq_zero h
    this.imp_left (@Subtype.ext_iff _ _ c 0).mpr⟩

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