map_iff — Mathlib

English

If f is injective, then Nilpotent is preserved and reflected: IsNilpotent(f(r)) iff IsNilpotent(r).

Русский

Если f инъективен, то нилпотентность сохраняется и восстанавливается: IsNilpotent(f(r)) ⇔ IsNilpotent(r).

LaTeX

$$$ \\text{Injective}(f) \\Rightarrow (\\IsNilpotent(f(r)) \\iff \\IsNilpotent(r)) $$$

Lean4

theorem map_iff [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*} [FunLike F R S] [MonoidWithZeroHomClass F R S]
    {f : F} (hf : Function.Injective f) : IsNilpotent (f r) ↔ IsNilpotent r :=
  ⟨fun ⟨k, hk⟩ ↦ ⟨k, (map_eq_zero_iff f hf).mp <| by rwa [map_pow]⟩, fun h ↦ h.map f⟩

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