charZero_iff — Mathlib

English

Let φ: R → S be an injective ring homomorphism. Then R has characteristic zero if and only if S has characteristic zero.

Русский

Пусть φ: R →+* S инъективен. Тогда характеристика нуля в R эквивалентна характеристике нуля в S.

LaTeX

$$$\\operatorname{charZero}(R) \\Rightarrow \\operatorname{charZero}(S) \\quad$ under $\\varphi$ injective$$

Lean4

theorem charZero_iff {ϕ : R →+* S} (hϕ : Injective ϕ) : CharZero R ↔ CharZero S :=
  ⟨fun hR => ⟨by intro a b h; rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]⟩, fun _ => ϕ.charZero⟩

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