int_of_charZero — Mathlib

English

If R is a ring with CharZero and M is a module with NoZeroSMulDivisors R M, then NoZeroSMulDivisors Int M holds.

Русский

Если R имеет характеристику ноль и M — модуль с NoZeroSMulDivisors R M, тогда NoZeroSMulDivisors ℤ M выполняется.

LaTeX

$$NoZeroSMulDivisors \mathbb{Z} M$$

Lean4

theorem int_of_charZero (R) (M) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] :
    NoZeroSMulDivisors ℤ M :=
  ⟨fun {z x} h ↦ by simpa [← smul_one_smul R z x] using h⟩

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