ringHom_map_cast — Mathlib

English

For any nonassociative ring R, any ring homomorphism f : R →+* ZMod n satisfies that for every k ∈ ZMod n, f(cast k) = k.

Русский

Для любой ненеразложенной кольцевой структуры R и гомоморфизма f : R →+* ZMod n верно, что для каждого k ∈ ZMod n выполняется f(cast k) = k.

LaTeX

$$$[\text{NonAssocRing } R] \ (f : R \to+* ZMod\ n)\; (k : ZMod\ n)\;:\; f (cast\ k) = k$$$

Lean4

@[simp]
theorem ringHom_map_cast [NonAssocRing R] (f : R →+* ZMod n) (k : ZMod n) : f (cast k) = k :=
  by
  cases n
  · dsimp [ZMod, ZMod.cast] at f k ⊢; simp
  · dsimp [ZMod.cast]
    rw [map_natCast, natCast_zmod_val]

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