of_mclosure_eq_top — Mathlib

English

Another instance of the explicit representation of the m-th power as n^m inside powers(n).

Русский

Ещё одно представление m-й степени как n^m внутри powers(n).

LaTeX

$$$ \\operatorname{pow}(n,m) = \\langle n^m, m, rfl \\rangle $$$

Lean4

@[to_additive]
theorem of_mclosure_eq_top {N α} [Monoid M] [SMul N α] [MulAction M α] {s : Set M} (htop : Submonoid.closure s = ⊤)
    (hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z) : SMulCommClass M N α :=
  by
  refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
  · intro y z
    rw [one_smul, one_smul]
  · clear x
    intro x hx x' hx' y z
    rw [mul_smul, mul_smul, hx', hs x hx]

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