instOfFaithfulSMul — Mathlib

English

If A has NoZeroSMulDivisors and R acts faithfully on A, then NoZeroSMulDivisors R A holds.

Русский

Если A не имеет нулевых делителей под действием и R действует достоверно на A, то NoZeroSMulDivisors R A верно.

LaTeX

$$$\mathrm{NoZeroSMulDivisors}\; R\; A.$$$

Lean4

instance (priority := 100) instOfFaithfulSMul {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    [NoZeroDivisors A] [FaithfulSMul R A] : NoZeroSMulDivisors R A :=
  ⟨fun hcx =>
    (mul_eq_zero.mp ((Algebra.smul_def _ _).symm.trans hcx)).imp_left
      (map_eq_zero_iff (algebraMap R A) <| FaithfulSMul.algebraMap_injective R A).mp⟩

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