instIsAddTorsionFreeOfCharZero — Mathlib

English

In a domain of characteristic zero, the additive structure is torsion-free: if n·a = 0 with n ≠ 0, then a = 0.

Русский

В домене нулевой характеристики аддитивная структура безторсионна: если n·a = 0 и n ≠ 0, то a = 0.

LaTeX

$$$\text{IsAddTorsionFree } R\text{ for char 0 domain}$$$

Lean4

scoped instance (R : Type*) [Semiring R] [IsDomain R] [CharZero R] : IsAddTorsionFree R where
  nsmul_right_injective n h a b
    w := by
    simp only [nsmul_eq_mul, mul_eq_mul_left_iff, Nat.cast_eq_zero] at w
    grind

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