charZero_of_inj_zero — Mathlib

English

If an additive monoid hom e: M → N satisfies e(1) = 1 and is injective, then N has characteristic zero.

Русский

Если непереходящий гомоморфизм аддитивных моноидов e: M → N удовлетворяет e(1) = 1 и инъективен, то N имеет характеристику ноль.

LaTeX

$$CharZero N where cast_injective n m h := by ...$$

Lean4

theorem charZero_of_inj_zero [AddGroupWithOne R] (H : ∀ n : ℕ, (n : R) = 0 → n = 0) : CharZero R :=
  ⟨@fun m n h => by
      induction m generalizing n with
      | zero => rw [H n]; rw [← h, Nat.cast_zero]
      | succ m ih =>
        cases n
        · apply H; rw [h, Nat.cast_zero]
        · simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]⟩

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