pow_exponent_eq_one — Mathlib

English

In a Submonoid S of G, for any g ∈ S, g^{exponent S} = 1.

Русский

В подмоноиде S для любого g ∈ S верно g^{exponent S} = 1.

LaTeX

$$$\\\\forall {S : Submonoid G} {g : G}, g \\in S \\\\Rightarrow g^{\\\\operatorname{exponent} S} = 1$$$

Lean4

@[to_additive]
theorem _root_.Submonoid.pow_exponent_eq_one {S : Submonoid G} {g : G} (g_in_s : g ∈ S) : g ^ (Monoid.exponent S) = 1 :=
  by
  have := Monoid.pow_exponent_eq_one (⟨g, g_in_s⟩ : S)
  rwa [SubmonoidClass.mk_pow, ← OneMemClass.coe_eq_one] at this

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