instFaithfulSMulOfNontrivial — Mathlib

English

If A is a domain, NoZeroSMulDivisors R A is equivalent to FaithfulSMul R A.

Русский

Если A — домен, тогда NoZeroSMulDivisors R A эквивалентно FaithfulSMul R A.

LaTeX

$$$\text{IsDomain}(A) \;\Rightarrow\; (\mathrm{NoZeroSMulDivisors}\; R\; A) \iff \mathrm{FaithfulSMul}\; R\; A.$$$

Lean4

instance [Nontrivial A] [NoZeroSMulDivisors R A] : FaithfulSMul R A where
  eq_of_smul_eq_smul {r₁ r₂}
    h := by
    specialize h 1
    rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero] at h
    exact h.resolve_right one_ne_zero

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