Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Jeremy Avigad, Robert Y. Lewis

! This file was ported from Lean 3 source module algebra.group_power.basic
! leanprover-community/mathlib commit 9b2660e1b25419042c8da10bf411aa3c67f14383
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Algebra.Group.Commute
import Mathlib.Algebra.Group.TypeTags

/-!
# Power operations on monoids and groups

The power operation on monoids and groups.
We separate this from group, because it depends on `ℕ`,
which in turn depends on other parts of algebra.

This module contains lemmas about `a ^ n` and `n • a`, where `n : ℕ` or `n : ℤ`.
Further lemmas can be found in `Algebra.GroupPower.Lemmas`.

The analogous results for groups with zero can be found in `Algebra.GroupWithZero.Power`.

## Notation

- `a ^ n` is used as notation for `Pow.pow a n`; in this file `n : ℕ` or `n : ℤ`.
- `n • a` is used as notation for `SMul.smul n a`; in this file `n : ℕ` or `n : ℤ`.

## Implementation details

We adopt the convention that `0^0 = 1`.
-/

universe u v w x y z u₁ u₂

variable {α: Type ?u.2α : Type _: Type (?u.21+1)Type _} {M: Type uM : Type u: Type (u+1)Type u} {N: Type vN : Type v: Type (v+1)Type v} {G: Type wG : Type w: Type (w+1)Type w} {H: Type xH : Type x: Type (x+1)Type x} {A: Type yA : Type y: Type (y+1)Type y} {B: Type zB : Type z: Type (z+1)Type z}
{R: Type u₁R : Type u₁: Type (u₁+1)Type u₁} {S: Type u₂S : Type u₂: Type (u₂+1)Type u₂}

/-!
### Commutativity

First we prove some facts about `SemiconjBy` and `Commute`. They do not require any theory about
`pow` and/or `nsmul` and will be useful later in this file.
-/

section Pow

variable [Pow: Type ?u.4449 → Type ?u.4448 → Type (max?u.4449?u.4448)Pow M: Type uM ℕ: Typeℕ]

@[simp]
theorem pow_ite: ∀ {M : Type u} [inst : Pow M ℕ] (P : Prop) [inst_1 : Decidable P] (a : M) (b c : ℕ),
(a ^ if P then b else c) = if P then a ^ b else a ^ cpow_ite (P: PropP : Prop: TypeProp) [Decidable: Prop → TypeDecidable P: PropP] (a: Ma : M: Type uM) (b: ℕb c: ℕc : ℕ: Typeℕ) :
(a: Ma ^ if P: PropP then b: ℕb else c: ℕc) = if P: PropP then a: Ma ^ b: ℕb else a: Ma ^ c: ℕc := byGoals accomplished! 🐙 α: Type ?u.44M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa: Mb, c: ℕ(a ^ if P then b else c) = if P then a ^ b else a ^ csplit_ifsα: Type ?u.44M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa: Mb, c: ℕh✝: Pinla ^ b = a ^ bα: Type ?u.44M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa: Mb, c: ℕh✝: ¬Pinra ^ c = a ^ c α: Type ?u.44M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa: Mb, c: ℕ(a ^ if P then b else c) = if P then a ^ b else a ^ c<;>α: Type ?u.44M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa: Mb, c: ℕh✝: Pinla ^ b = a ^ bα: Type ?u.44M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa: Mb, c: ℕh✝: ¬Pinra ^ c = a ^ c α: Type ?u.44M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa: Mb, c: ℕ(a ^ if P then b else c) = if P then a ^ b else a ^ crflGoals accomplished! 🐙
#align pow_ite pow_ite: ∀ {M : Type u} [inst : Pow M ℕ] (P : Prop) [inst_1 : Decidable P] (a : M) (b c : ℕ),
(a ^ if P then b else c) = if P then a ^ b else a ^ cpow_ite

@[simp]
theorem ite_pow: ∀ {M : Type u} [inst : Pow M ℕ] (P : Prop) [inst_1 : Decidable P] (a b : M) (c : ℕ),
(if P then a else b) ^ c = if P then a ^ c else b ^ cite_pow (P: PropP : Prop: TypeProp) [Decidable: Prop → TypeDecidable P: PropP] (a: Ma b: Mb : M: Type uM) (c: ℕc : ℕ: Typeℕ) :
(if P: PropP then a: Ma else b: Mb) ^ c: ℕc = if P: PropP then a: Ma ^ c: ℕc else b: Mb ^ c: ℕc := byGoals accomplished! 🐙 α: Type ?u.4429M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa, b: Mc: ℕ(if P then a else b) ^ c = if P then a ^ c else b ^ csplit_ifsα: Type ?u.4429M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa, b: Mc: ℕh✝: Pinla ^ c = a ^ cα: Type ?u.4429M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa, b: Mc: ℕh✝: ¬Pinrb ^ c = b ^ c α: Type ?u.4429M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa, b: Mc: ℕ(if P then a else b) ^ c = if P then a ^ c else b ^ c<;>α: Type ?u.4429M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa, b: Mc: ℕh✝: Pinla ^ c = a ^ cα: Type ?u.4429M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa, b: Mc: ℕh✝: ¬Pinrb ^ c = b ^ c α: Type ?u.4429M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Pow M ℕP: Propinst✝: Decidable Pa, b: Mc: ℕ(if P then a else b) ^ c = if P then a ^ c else b ^ crflGoals accomplished! 🐙
#align ite_pow ite_pow: ∀ {M : Type u} [inst : Pow M ℕ] (P : Prop) [inst_1 : Decidable P] (a b : M) (c : ℕ),
(if P then a else b) ^ c = if P then a ^ c else b ^ cite_pow

end Pow

/-!
### Monoids
-/

section Monoid

variable [Monoid: Type ?u.12784 → Type ?u.12784Monoid M: Type uM] [AddMonoid: Type ?u.8659 → Type ?u.8659AddMonoid A: Type yA]

theorem nsmul_zero: ∀ {A : Type y} [inst : AddMonoid A] (n : ℕ), n • 0 = 0nsmul_zero (n: ℕn : ℕ: Typeℕ) : n: ℕn • (0: ?m.87000 : A: Type yA) = 0: ?m.88800 := byGoals accomplished! 🐙
α: Type ?u.8662M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕn • 0 = 0induction' n: ℕn with n: ℕn ih: ?m.8912 nihα: Type ?u.8662M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid AzeroNat.zero • 0 = 0α: Type ?u.8662M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: n • 0 = 0succNat.succ n • 0 = 0
α: Type ?u.8662M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕn • 0 = 0·α: Type ?u.8662M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid AzeroNat.zero • 0 = 0 α: Type ?u.8662M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid AzeroNat.zero • 0 = 0α: Type ?u.8662M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: n • 0 = 0succNat.succ n • 0 = 0exact zero_nsmul: ∀ {M : Type ?u.8923} [inst : AddMonoid M] (a : M), 0 • a = 0zero_nsmul _: ?m.8924_Goals accomplished! 🐙
#align nsmul_zero nsmul_zero: ∀ {A : Type y} [inst : AddMonoid A] (n : ℕ), n • 0 = 0nsmul_zero

@[simp]
#align one_nsmul one_nsmul: ∀ {A : Type y} [inst : AddMonoid A] (a : A), 1 • a = aone_nsmul

theorem add_nsmul: ∀ (a : A) (m n : ℕ), (m + n) • a = m • a + n • aadd_nsmul (a: Aa : A: Type yA) (m: ℕm n: ℕn : ℕ: Typeℕ) : (m: ℕm + n: ℕn) • a: Aa = m: ℕm • a: Aa + n: ℕn • a: Aa := byGoals accomplished! 🐙
α: Type ?u.9319M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Am, n: ℕ(m + n) • a = m • a + n • ainduction m: ℕm with
#align add_nsmul add_nsmul: ∀ {A : Type y} [inst : AddMonoid A] (a : A) (m n : ℕ), (m + n) • a = m • a + n • aadd_nsmul

-- the attributes are intentionally out of order.
@[to_additive existing nsmul_zero: ∀ {A : Type y} [inst : AddMonoid A] (n : ℕ), n • 0 = 0nsmul_zero, simp]
theorem one_pow: ∀ (n : ℕ), 1 ^ n = 1one_pow (n: ℕn : ℕ: Typeℕ) : (1: ?m.98741 : M: Type uM) ^ n: ℕn = 1: ?m.99721 := byGoals accomplished! 🐙
α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕ1 ^ n = 1induction' n: ℕn with n: ℕn ih: ?m.11293 nihα: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Azero1 ^ Nat.zero = 1α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 ^ Nat.succ n = 1
α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕ1 ^ n = 1·α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Azero1 ^ Nat.zero = 1 α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Azero1 ^ Nat.zero = 1α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 ^ Nat.succ n = 1exact pow_zero: ∀ {M : Type ?u.11304} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero _: ?m.11305_Goals accomplished! 🐙
α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕ1 ^ n = 1·α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 ^ Nat.succ n = 1 α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 ^ Nat.succ n = 1rw [α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 ^ Nat.succ n = 1pow_succ: ∀ {M : Type ?u.11340} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ npow_succ,α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 * 1 ^ n = 1 α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 ^ Nat.succ n = 1ih: ?m.11293 nih,α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 * 1 = 1 α: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 ^ Nat.succ n = 1one_mul: ∀ {M : Type ?u.11378} [inst : MulOneClass M] (a : M), 1 * a = aone_mulα: Type ?u.9841M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid An: ℕih: 1 ^ n = 1succ1 = 1]Goals accomplished! 🐙
#align one_pow one_pow: ∀ {M : Type u} [inst : Monoid M] (n : ℕ), 1 ^ n = 1one_pow

@[to_additive existing (attr := simp) one_nsmul: ∀ {A : Type y} [inst : AddMonoid A] (a : A), 1 • a = aone_nsmul]
theorem pow_one: ∀ (a : M), a ^ 1 = apow_one (a: Ma : M: Type uM) : a: Ma ^ 1: ?m.115251 = a: Ma := byGoals accomplished! 🐙 α: Type ?u.11493M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 1 = arw [α: Type ?u.11493M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 1 = apow_succ: ∀ {M : Type ?u.11675} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ npow_succ,α: Type ?u.11493M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma * a ^ 0 = a α: Type ?u.11493M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 1 = apow_zero: ∀ {M : Type ?u.11715} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero,α: Type ?u.11493M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma * 1 = a α: Type ?u.11493M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 1 = amul_one: ∀ {M : Type ?u.11742} [inst : MulOneClass M] (a : M), a * 1 = amul_oneα: Type ?u.11493M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma = a]Goals accomplished! 🐙
#align pow_one pow_one: ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 1 = apow_one

/-- Note that most of the lemmas about powers of two refer to it as `sq`. -/
@[to_additive two_nsmul: ∀ {M : Type u} [inst : AddMonoid M] (a : M), 2 • a = a + atwo_nsmul ""]
theorem pow_two: ∀ (a : M), a ^ 2 = a * apow_two (a: Ma : M: Type uM) : a: Ma ^ 2: ?m.119012 = a: Ma * a: Ma := byGoals accomplished! 🐙 α: Type ?u.11869M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 2 = a * arw [α: Type ?u.11869M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 2 = a * apow_succ: ∀ {M : Type ?u.12197} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ npow_succ,α: Type ?u.11869M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma * a ^ 1 = a * a α: Type ?u.11869M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 2 = a * apow_one: ∀ {M : Type ?u.12237} [inst : Monoid M] (a : M), a ^ 1 = apow_oneα: Type ?u.11869M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma * a = a * a]Goals accomplished! 🐙
#align pow_two pow_two: ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 2 = a * apow_two
#align two_nsmul two_nsmul: ∀ {M : Type u} [inst : AddMonoid M] (a : M), 2 • a = a + atwo_nsmul

alias pow_two: ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 2 = a * apow_two ← sq: ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 2 = a * asq
#align sq sq: ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 2 = a * asq

theorem pow_three': ∀ (a : M), a ^ 3 = a * a * apow_three' (a: Ma : M: Type uM) : a: Ma ^ 3: ?m.123203 = a: Ma * a: Ma * a: Ma := byGoals accomplished! 🐙 α: Type ?u.12288M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 3 = a * a * arw [α: Type ?u.12288M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 3 = a * a * apow_succ': ∀ {M : Type ?u.12688} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a ^ n * apow_succ',α: Type ?u.12288M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 2 * a = a * a * a α: Type ?u.12288M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 3 = a * a * apow_two: ∀ {M : Type ?u.12728} [inst : Monoid M] (a : M), a ^ 2 = a * apow_twoα: Type ?u.12288M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma * a * a = a * a * a]Goals accomplished! 🐙
#align pow_three' pow_three': ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 3 = a * a * apow_three'

theorem pow_three: ∀ (a : M), a ^ 3 = a * (a * a)pow_three (a: Ma : M: Type uM) : a: Ma ^ 3: ?m.127973 = a: Ma * (a: Ma * a: Ma) := byGoals accomplished! 🐙 α: Type ?u.12765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 3 = a * (a * a)rw [α: Type ?u.12765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 3 = a * (a * a)pow_succ: ∀ {M : Type ?u.13165} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ npow_succ,α: Type ?u.12765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma * a ^ 2 = a * (a * a) α: Type ?u.12765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma ^ 3 = a * (a * a)pow_two: ∀ {M : Type ?u.13205} [inst : Monoid M] (a : M), a ^ 2 = a * apow_twoα: Type ?u.12765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Ma * (a * a) = a * (a * a)]Goals accomplished! 🐙
#align pow_three pow_three: ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 3 = a * (a * a)pow_three

@[to_additive existing add_nsmul: ∀ {A : Type y} [inst : AddMonoid A] (a : A) (m n : ℕ), (m + n) • a = m • a + n • aadd_nsmul]
theorem pow_add: ∀ (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ npow_add (a: Ma : M: Type uM) (m: ℕm n: ℕn : ℕ: Typeℕ) : a: Ma ^ (m: ℕm + n: ℕn) = a: Ma ^ m: ℕm * a: Ma ^ n: ℕn := byGoals accomplished! 🐙
α: Type ?u.13242M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (m + n) = a ^ m * a ^ ninduction' n: ℕn with n: ℕn ih: ?m.14761 nihα: Type ?u.13242M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzeroa ^ (m + Nat.zero) = a ^ m * a ^ Nat.zeroα: Type ?u.13242M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕih: a ^ (m + n) = a ^ m * a ^ nsucca ^ (m + Nat.succ n) = a ^ m * a ^ Nat.succ n
#align pow_add pow_add: ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ npow_add

@[to_additive mul_nsmul: ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), (m * n) • a = n • m • amul_nsmul]
theorem pow_mul: ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ npow_mul (a: Ma : M: Type uM) (m: ℕm n: ℕn : ℕ: Typeℕ) : a: Ma ^ (m: ℕm * n: ℕn) = (a: Ma ^ m: ℕm) ^ n: ℕn := byGoals accomplished! 🐙
α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (m * n) = (a ^ m) ^ ninduction' n: ℕn with n: ℕn ih: ?m.16524 nihα: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzeroa ^ (m * Nat.zero) = (a ^ m) ^ Nat.zeroα: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕih: a ^ (m * n) = (a ^ m) ^ nsucca ^ (m * Nat.succ n) = (a ^ m) ^ Nat.succ n
α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (m * n) = (a ^ m) ^ n·α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzeroa ^ (m * Nat.zero) = (a ^ m) ^ Nat.zero α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzeroa ^ (m * Nat.zero) = (a ^ m) ^ Nat.zeroα: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕih: a ^ (m * n) = (a ^ m) ^ nsucca ^ (m * Nat.succ n) = (a ^ m) ^ Nat.succ nrw [α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzeroa ^ (m * Nat.zero) = (a ^ m) ^ Nat.zeroNat.mul_zero: ∀ (n : ℕ), n * 0 = 0Nat.mul_zero,α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzeroa ^ 0 = (a ^ m) ^ Nat.zero α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzeroa ^ (m * Nat.zero) = (a ^ m) ^ Nat.zeropow_zero: ∀ {M : Type ?u.16546} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero,α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzero1 = (a ^ m) ^ Nat.zero α: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzeroa ^ (m * Nat.zero) = (a ^ m) ^ Nat.zeropow_zero: ∀ {M : Type ?u.16590} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zeroα: Type ?u.15094M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm: ℕzero1 = 1]Goals accomplished! 🐙
-- Porting note: we are taking the opportunity to swap the names `mul_nsmul` and `mul_nsmul'`
-- using #align, so that in mathlib4 they will match the multiplicative ones.
#align pow_mul pow_mul: ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ npow_mul
#align mul_nsmul' mul_nsmul: ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), (m * n) • a = n • m • amul_nsmul

@[to_additive mul_nsmul': ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), (m * n) • a = m • n • amul_nsmul']
theorem pow_mul': ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ n) ^ mpow_mul' (a: Ma : M: Type uM) (m: ℕm n: ℕn : ℕ: Typeℕ) : a: Ma ^ (m: ℕm * n: ℕn) = (a: Ma ^ n: ℕn) ^ m: ℕm := byGoals accomplished! 🐙 α: Type ?u.16765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (m * n) = (a ^ n) ^ mrw [α: Type ?u.16765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (m * n) = (a ^ n) ^ mNat.mul_comm: ∀ (n m : ℕ), n * m = m * nNat.mul_comm,α: Type ?u.16765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (n * m) = (a ^ n) ^ m α: Type ?u.16765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (m * n) = (a ^ n) ^ mpow_mul: ∀ {M : Type ?u.18196} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ npow_mulα: Type ?u.16765M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕ(a ^ n) ^ m = (a ^ n) ^ m]Goals accomplished! 🐙
#align pow_mul' pow_mul': ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ n) ^ mpow_mul'
#align mul_nsmul mul_nsmul': ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), (m * n) • a = m • n • amul_nsmul'

@[to_additive: ∀ {M : Type u} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), n • (a + b) = n • a + n • bto_additive]
theorem Commute.mul_pow: ∀ {a b : M}, Commute a b → ∀ (n : ℕ), (a * b) ^ n = a ^ n * b ^ nCommute.mul_pow {a: Ma b: Mb : M: Type uM} (h: Commute a bh : Commute: {S : Type ?u.18307} → [inst : Mul S] → S → S → PropCommute a: Ma b: Mb) (n: ℕn : ℕ: Typeℕ) : (a: Ma * b: Mb) ^ n: ℕn = a: Ma ^ n: ℕn * b: Mb ^ n: ℕn := byGoals accomplished! 🐙
α: Type ?u.18278M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa, b: Mh: Commute a bn: ℕ(a * b) ^ n = a ^ n * b ^ ninduction' n: ℕn with n: ℕn ih: ?m.19911 nihα: Type ?u.18278M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa, b: Mh: Commute a bzero(a * b) ^ Nat.zero = a ^ Nat.zero * b ^ Nat.zeroα: Type ?u.18278M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa, b: Mh: Commute a bn: ℕih: (a * b) ^ n = a ^ n * b ^ nsucc(a * b) ^ Nat.succ n = a ^ Nat.succ n * b ^ Nat.succ n
α: Type ?u.18278M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa, b: Mh: Commute a bn: ℕ(a * b) ^ n = a ^ n * b ^ n·α: Type ?u.18278M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa, b: Mh: Commute a bn: ℕih: (a * b) ^ n = a ^ n * b ^ nsucc(a * b) ^ Nat.succ n = a ^ Nat.succ n * b ^ Nat.succ n α: Type ?u.18278M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa, b: Mh: Commute a bn: ℕih: (a * b) ^ n = a ^ n * b ^ nsucc(a * b) ^ Nat.succ n = a ^ Nat.succ n * b ^ Nat.succ nsimp only [pow_succ: ∀ {M : Type ?u.20107} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ npow_succ, ih: ?m.19911 nih, ← mul_assoc: ∀ {G : Type ?u.20124} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc, (h: Commute a bh.pow_left: ∀ {M : Type ?u.20148} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute (a ^ n) bpow_left n: ℕn).right_comm: ∀ {S : Type ?u.20176} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a : S), a * b * c = a * c * bright_comm]Goals accomplished! 🐙
#align commute.mul_pow Commute.mul_pow: ∀ {M : Type u} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), (a * b) ^ n = a ^ n * b ^ nCommute.mul_pow

@[to_additive: ∀ {M : Type u} [inst : AddMonoid M] (a : M) (n : ℕ), n • a + a = a + n • ato_additive]
theorem pow_mul_comm': ∀ (a : M) (n : ℕ), a ^ n * a = a * a ^ npow_mul_comm' (a: Ma : M: Type uM) (n: ℕn : ℕ: Typeℕ) : a: Ma ^ n: ℕn * a: Ma = a: Ma * a: Ma ^ n: ℕn :=
Commute.pow_self: ∀ {M : Type ?u.22114} [inst : Monoid M] (a : M) (n : ℕ), Commute (a ^ n) aCommute.pow_self a: Ma n: ℕn
#align pow_mul_comm' pow_mul_comm': ∀ {M : Type u} [inst : Monoid M] (a : M) (n : ℕ), a ^ n * a = a * a ^ npow_mul_comm'
#align nsmul_add_comm' nsmul_add_comm': ∀ {M : Type u} [inst : AddMonoid M] (a : M) (n : ℕ), n • a + a = a + n • ansmul_add_comm'

theorem pow_boole: ∀ (P : Prop) [inst : Decidable P] (a : M), (a ^ if P then 1 else 0) = if P then a else 1pow_boole (P: PropP : Prop: TypeProp) [Decidable: Prop → TypeDecidable P: PropP] (a: Ma : M: Type uM) :
(a: Ma ^ if P: PropP then 1: ?m.221841 else 0: ?m.221950) = if P: PropP then a: Ma else 1: ?m.222191 := byGoals accomplished! 🐙 α: Type ?u.22144M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝²: Monoid Minst✝¹: AddMonoid AP: Propinst✝: Decidable Pa: M(a ^ if P then 1 else 0) = if P then a else 1simpGoals accomplished! 🐙
#align pow_boole pow_boole: ∀ {M : Type u} [inst : Monoid M] (P : Prop) [inst_1 : Decidable P] (a : M),
(a ^ if P then 1 else 0) = if P then a else 1pow_boole

@[to_additive nsmul_left_comm: ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), n • m • a = m • n • ansmul_left_comm]
theorem pow_right_comm: ∀ (a : M) (m n : ℕ), (a ^ m) ^ n = (a ^ n) ^ mpow_right_comm (a: Ma : M: Type uM) (m: ℕm n: ℕn : ℕ: Typeℕ) : (a: Ma ^ m: ℕm) ^ n: ℕn = (a: Ma ^ n: ℕn) ^ m: ℕm := byGoals accomplished! 🐙
α: Type ?u.22873M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕ(a ^ m) ^ n = (a ^ n) ^ mrw [α: Type ?u.22873M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕ(a ^ m) ^ n = (a ^ n) ^ m← pow_mul: ∀ {M : Type ?u.24293} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ npow_mul,α: Type ?u.22873M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (m * n) = (a ^ n) ^ m α: Type ?u.22873M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕ(a ^ m) ^ n = (a ^ n) ^ mNat.mul_comm: ∀ (n m : ℕ), n * m = m * nNat.mul_comm,α: Type ?u.22873M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕa ^ (n * m) = (a ^ n) ^ m α: Type ?u.22873M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕ(a ^ m) ^ n = (a ^ n) ^ mpow_mul: ∀ {M : Type ?u.24354} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ npow_mulα: Type ?u.22873M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕ(a ^ n) ^ m = (a ^ n) ^ m]Goals accomplished! 🐙
#align pow_right_comm pow_right_comm: ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), (a ^ m) ^ n = (a ^ n) ^ mpow_right_comm
#align nsmul_left_comm nsmul_left_comm: ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), n • m • a = m • n • ansmul_left_comm

@[to_additive nsmul_add_sub_nsmul: ∀ {M : Type u} [inst : AddMonoid M] (a : M) {m n : ℕ}, m ≤ n → m • a + (n - m) • a = n • ansmul_add_sub_nsmul]
theorem pow_mul_pow_sub: ∀ {M : Type u} [inst : Monoid M] (a : M) {m n : ℕ}, m ≤ n → a ^ m * a ^ (n - m) = a ^ npow_mul_pow_sub (a: Ma : M: Type uM) {m: ℕm n: ℕn : ℕ: Typeℕ} (h: m ≤ nh : m: ℕm ≤ n: ℕn) : a: Ma ^ m: ℕm * a: Ma ^ (n: ℕn - m: ℕm) = a: Ma ^ n: ℕn := byGoals accomplished! 🐙
#align pow_mul_pow_sub pow_mul_pow_sub: ∀ {M : Type u} [inst : Monoid M] (a : M) {m n : ℕ}, m ≤ n → a ^ m * a ^ (n - m) = a ^ npow_mul_pow_sub
#align nsmul_add_sub_nsmul nsmul_add_sub_nsmul: ∀ {M : Type u} [inst : AddMonoid M] (a : M) {m n : ℕ}, m ≤ n → m • a + (n - m) • a = n • ansmul_add_sub_nsmul

@[to_additive sub_nsmul_nsmul_add: ∀ {M : Type u} [inst : AddMonoid M] (a : M) {m n : ℕ}, m ≤ n → (n - m) • a + m • a = n • asub_nsmul_nsmul_add]
theorem pow_sub_mul_pow: ∀ {M : Type u} [inst : Monoid M] (a : M) {m n : ℕ}, m ≤ n → a ^ (n - m) * a ^ m = a ^ npow_sub_mul_pow (a: Ma : M: Type uM) {m: ℕm n: ℕn : ℕ: Typeℕ} (h: m ≤ nh : m: ℕm ≤ n: ℕn) : a: Ma ^ (n: ℕn - m: ℕm) * a: Ma ^ m: ℕm = a: Ma ^ n: ℕn := byGoals accomplished! 🐙
α: Type ?u.26055M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕh: m ≤ na ^ (n - m) * a ^ m = a ^ nrw [α: Type ?u.26055M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕh: m ≤ na ^ (n - m) * a ^ m = a ^ n← pow_add: ∀ {M : Type ?u.27570} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ npow_add,α: Type ?u.26055M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕh: m ≤ na ^ (n - m + m) = a ^ n α: Type ?u.26055M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕh: m ≤ na ^ (n - m) * a ^ m = a ^ nNat.sub_add_cancel: ∀ {n m : ℕ}, m ≤ n → n - m + m = nNat.sub_add_cancel h: m ≤ nhα: Type ?u.26055M: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝¹: Monoid Minst✝: AddMonoid Aa: Mm, n: ℕh: m ≤ na ^ n = a ^ n]Goals accomplished! 🐙
#align pow_sub_mul_pow pow_sub_mul_pow: ∀ {M : Type u} [inst : Monoid M] (a : M) {m n : ℕ}, m ≤ n → a ^ (n - m) * a ^ m = a ^ npow_sub_mul_pow
#align sub_nsmul_nsmul_add sub_nsmul_nsmul_add: ∀ {M : Type u} [inst : AddMonoid M] (a : M) {m n : ℕ}, m ≤ n → (n - m) • a + m • a = n • asub_nsmul_nsmul_add

/-- If `x ^ n = 1`, then `x ^ m` is the same as `x ^ (m % n)` -/
@[to_additive nsmul_eq_mod_nsmul: ∀ {M : Type u_1} [inst : AddMonoid M] {x : M} (m : ℕ) {n : ℕ}, n • x = 0 → m • x = (m % n) • xnsmul_eq_mod_nsmul "If `n • x = 0`, then `m • x` is the same as `(m % n) • x`"]
theorem pow_eq_pow_mod: ∀ {M : Type u_1} [inst : Monoid M] {x : M} (m : ℕ) {n : ℕ}, x ^ n = 1 → x ^ m = x ^ (m % n)pow_eq_pow_mod {M: Type ?u.27699M : Type _: Type (?u.27699+1)Type _} [Monoid: Type ?u.27702 → Type ?u.27702Monoid M: Type ?u.27699M] {x: Mx : M: Type ?u.27699M} (m: ℕm : ℕ: Typeℕ) {n: ℕn : ℕ: Typeℕ} (h: x ^ n = 1h : x: Mx ^ n: ℕn = 1: ?m.277161) :
x: Mx ^ m: ℕm = x: Mx ^ (m: ℕm % n: ℕn) := byGoals accomplished! 🐙
α: Type ?u.27674M✝: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝²: Monoid M✝inst✝¹: AddMonoid AM: Type u_1inst✝: Monoid Mx: Mm, n: ℕh: x ^ n = 1x ^ m = x ^ (m % n)have t: x ^ m = x ^ (n * (m / n) + m % n)t : x: Mx ^ m: ℕm = x: Mx ^ (n: ℕn * (m: ℕm / n: ℕn) + m: ℕm % n: ℕn) :=
congr_arg: ∀ {α : Sort ?u.31834} {β : Sort ?u.31833} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congr_arg (fun a: ?m.31840a => x: Mx ^ a: ?m.31840a) ((Nat.add_comm: ∀ (n m : ℕ), n + m = m + nNat.add_comm _: ℕ_ _: ℕ_).trans: ∀ {α : Sort ?u.31938} {a b c : α}, a = b → b = c → a = ctrans (Nat.mod_add_div: ∀ (m k : ℕ), m % k + k * (m / k) = mNat.mod_add_div _: ℕ_ _: ℕ_)).symm: ∀ {α : Sort ?u.31960} {a b : α}, a = b → b = asymmα: Type ?u.27674M✝: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝²: Monoid M✝inst✝¹: AddMonoid AM: Type u_1inst✝: Monoid Mx: Mm, n: ℕh: x ^ n = 1t: x ^ m = x ^ (n * (m / n) + m % n)x ^ m = x ^ (m % n)
α: Type ?u.27674M✝: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝²: Monoid M✝inst✝¹: AddMonoid AM: Type u_1inst✝: Monoid Mx: Mm, n: ℕh: x ^ n = 1x ^ m = x ^ (m % n)dsimp at t: x ^ m = x ^ (n * (m / n) + m % n)tα: Type ?u.27674M✝: Type uN: Type vG: Type wH: Type xA: Type yB: Type zR: Type u₁S: Type u₂inst✝²: Monoid M✝inst✝¹: AddMonoid AM: Type u_1inst✝: Monoid Mx: Mm, n: ℕh: x ^ n = 1t: x ^ m = x ^ (n * (m / n) + m % n)x ^ m = x ^ (m % n)
#align pow_eq_pow_mod pow_eq_pow_mod: ∀ {M : Type u_1} [inst : Monoid M] {x : M} (m : ℕ) {n : ℕ}, x ^ n = 1 → x ^ m = x ^ (m % n)pow_eq_pow_mod
#align nsmul_eq_mod_nsmul nsmul_eq_mod_nsmul: ∀ {M : Type u_1} [inst : AddMonoid M] {x : M} (m : ℕ) {n : ℕ}, n • x = 0 → m • x = (m % n) • xnsmul_eq_mod_nsmul

@[to_additive: ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), m • a + n • a = n • a + m • ato_additive]
theorem pow_mul_comm: ∀ (a : M) (m n : ℕ), a ^ m * a ^ n = a ^ n * a ^ mpow_mul_comm (a: Ma : M: Type uM) (m: ℕm n: ℕn : ℕ: Typeℕ) : a: Ma ^ m: ℕm * a: Ma ^ n: ℕn = a: Ma ^ n: ℕn * a: Ma ^ m: ℕm :=
Commute.pow_pow_self: ∀ {M : Type ?u.33835} [inst : Monoid M] (a : M) (m n : ℕ), Commute (a ^ m) (a ^ n)Commute.pow_pow_self a: Ma m: ℕm n: ℕn
#align pow_mul_comm pow_mul_comm: ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ m * a ^ n = a ^ n * a ^ mpow_mul_comm
#align nsmul_add_comm nsmul_add_comm: ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), m • a + n • a = n • a + m • ansmul_add_comm

section Bit

set_option linter.deprecated false

@[to_additive bit0_nsmul: ∀ {M : Type u} [inst : AddMonoid M] (a : M) (n : ℕ), bit0 n • a = n • a + n • abit0_nsmul]
theorem ```