toZModPow_eq_iff_ext — Mathlib

English

The extensional principle for toZModPow: if two ring homomorphisms g,g' R → ℤ_[p] agree after all toZModPow n projections, then g = g'.

Русский

Принцип экстенсиональности для toZModPow: если два гомоморфизма g,g' совпадают после всех проекций toZModPow n, то g = g'.

LaTeX

$$$\\big( \\forall n, (toZModPow\\, n) \\circ g = (toZModPow\\, n) \\circ g' \\big) \\Rightarrow g = g'$$$

Lean4

theorem toZModPow_eq_iff_ext {R : Type*} [NonAssocSemiring R] {g g' : R →+* ℤ_[p]} :
    (∀ n, (toZModPow n).comp g = (toZModPow n).comp g') ↔ g = g' :=
  by
  constructor
  · intro hg
    ext x : 1
    apply ext_of_toZModPow.mp
    intro n
    change (toZModPow n).comp g x = (toZModPow n).comp g' x
    rw [hg n]
  · rintro rfl _
    rfl

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