pow — Mathlib

English

If a is inseparable from b, then a^n is inseparable from b^n for every n.

Русский

Если a неразделим с b, то a^n неразделим с b^n для каждого n.

LaTeX

$$$\text{Inseparable}(a,b) \Rightarrow \forall n: \mathbb{N},\ \text{Inseparable}(a^n,b^n)$$$

Lean4

@[to_additive]
protected theorem pow {M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a b : M} (h : Inseparable a b)
    (n : ℕ) : Inseparable (a ^ n) (b ^ n) :=
  (h.specializes.pow n).antisymm (h.specializes'.pow n)

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