ringHom_rightInverse — Mathlib

English

For any nonassociative ring R and any ring hom f : R →+* ZMod n, there exists a right inverse to f, namely cast, so that cast ∘ f = id_R.

Русский

Для любого неассоциативного кольца R и гомоморфизма f : R →+* ZMod n существует правая обратная к f, на самом деле cast, так что cast ∘ f = id_R.

LaTeX

$$$\exists \text{RightInverse }(\text{cast})\ f$$$

Lean4

/-- Any ring homomorphism into `ZMod n` has a right inverse. -/
theorem ringHom_rightInverse [NonAssocRing R] (f : R →+* ZMod n) : Function.RightInverse (cast : ZMod n → R) f :=
  ringHom_map_cast f

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