zpowers_isMulCommutative — Mathlib

English

For any g ∈ G, the range of zpowersHom G g is exactly zpowers g: (zpowersHom G g).range = zpowers g.

Русский

Для любого g ∈ G область определения zpowersHom G g равна zpowers g: диапазон zpowersHom g = zpowers g.

LaTeX

$$$\text{range}(\,zpowersHom\, G\, g\,) = \operatorname{zpowers}(g)$$$

Lean4

@[to_additive]
instance zpowers_isMulCommutative (g : G) : IsMulCommutative (zpowers g) :=
  ⟨⟨fun ⟨_, _, h₁⟩ ⟨_, _, h₂⟩ => by
      rw [Subtype.ext_iff, coe_mul, coe_mul, Subtype.coe_mk, Subtype.coe_mk, ← h₁, ← h₂, zpow_mul_comm]⟩⟩

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