of_noZeroSMulDivisors — Mathlib

English

If M is a nontrivial additive monoid with one and a module structure over R, and M has CharZero, then R has CharZero.

Русский

Если M является ненулевым аддитивным моноидом с единицей и модульной структурой над R, и у M есть CharZero, то характеристика R равна нулю.

LaTeX

$$CharZero R$$

Lean4

/-- Only a ring of characteristic zero can have a non-trivial module without additive or
scalar torsion. -/
theorem of_noZeroSMulDivisors [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R :=
  by
  refine ⟨fun {n m h} ↦ ?_⟩
  obtain ⟨x, hx⟩ := exists_ne (0 : M)
  replace h : (n : ℤ) • x = (m : ℤ) • x := by simp [← Nat.cast_smul_eq_nsmul R, h]
  simpa using smul_left_injective ℤ hx h

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