of_mclosure_eq_top — Mathlib

English

Repeatedly, the m-th power of n in the submonoid equals n^m with the same witness; identical to the earlier pow_apply statement.

Русский

Повторяющееся утверждение: m-я степень n в подмоноиде равна n^m с тем же свидетелем; соответствует предыдущему pow_apply.

LaTeX

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

Lean4

@[to_additive]
theorem of_mclosure_eq_top {N α} [Monoid M] [MulAction M N] [SMul N α] [MulAction M α] {s : Set M}
    (htop : Submonoid.closure s = ⊤) (hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z) : IsScalarTower 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, hs x hx, hx']

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