nat_of_injective — Mathlib

English

Let f: R → S be a ring homomorphism that is injective. If the natural number n is nonzero in R, then its image in S is nonzero; i.e., injective maps preserve nonzeroness of natural numbers.

Русский

Пусть f: R → S — инъективное кольцевое гомоморфизм. Если натуральное число n не равно нулю в R, то его образ в S не равен нулю; то есть инъекции сохраняют не нулевые натуральные числа.

LaTeX

$$If f: R → S is injective, then for all n ∈ ℕ, NeZero(n:R) ⇒ NeZero(n:S).$$

Lean4

theorem nat_of_injective {n : ℕ} [NeZero (n : R)] [RingHomClass F R S] {f : F} (hf : Function.Injective f) :
    NeZero (n : S) :=
  ⟨fun h ↦ NeZero.natCast_ne n R <| hf <| by simpa only [map_natCast, map_zero f]⟩

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