pow_toAddSubmonoid — Mathlib

English

Let M be a submodule of A. For n ≠ 0, the additive submonoid of M^n equals the n-th power of the additive submonoid of M.

Русский

Пусть M — подмодуль A. При n ≠ 0 аддитивный подпmonoid M^n совпадает с n-й степенью аддитивного подпmonoid M.

LaTeX

$$$ (M^{n}).toAddSubmonoid = M.toAddSubmonoid^{n} \quad (n \ne 0). $$$

Lean4

theorem pow_toAddSubmonoid {n : ℕ} (h : n ≠ 0) : (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n := by
  induction n with
  | zero => exact (h rfl).elim
  | succ n ih =>
    rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]
    cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]

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