monoidHomOfForallMemZpowers_apply_gen

English

The constructed homomorphism sends the generator g to g' in the generating setup.

Русский

Сгенерированный гомоморфизм отображает порождающий элемент g в g'.

LaTeX

$$monoidHomOfForallMemZpowers hg hg' g = g'$$

Lean4

@[to_additive (attr := simp)]
theorem monoidHomOfForallMemZpowers_apply_gen : monoidHomOfForallMemZpowers hg hg' g = g' :=
  by
  simp only [monoidHomOfForallMemZpowers, MonoidHom.coe_mk, OneHom.coe_mk]
  nth_rw 2 [← zpow_one g']
  rw [zpow_eq_zpow_iff_modEq]
  apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')
  rw [← zpow_eq_zpow_iff_modEq, zpow_one]
  exact Classical.choose_spec <| mem_zpowers_iff.mp <| hg g

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