pow_mul_pow_eq_one — Mathlib

English

If a b = 1, then a^n b^n = 1 for every n ≥ 0.

Русский

Если a b = 1, то a^n b^n = 1 для каждого n ≥ 0.

LaTeX

$$$ab = 1 \\Rightarrow a^{n} b^{n} = 1 \\quad (\\forall n \\in \\mathbb{N})$$$

Lean4

@[to_additive]
theorem pow_mul_pow_eq_one : ∀ n, a * b = 1 → a ^ n * b ^ n = 1
  | 0, _ => by simp
  | n + 1, h =>
    calc
      a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n) := by rw [pow_succ, pow_succ']
      _ = a ^ n * (a * b) * b ^ n := by simp only [mul_assoc]
      _ = 1 := by simp [h, pow_mul_pow_eq_one]

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