rootableByNatOfRootableByInt — Mathlib

English

If A is a group and α is ℤ-rootable, then A is ℕ-rootable by composing with the inclusion ℕ ↪ ℤ.

Русский

Если A — группа и ℤ-узел существует, то A является ℕ-узлом через включение ℕ в ℤ.

LaTeX

$$$\text{RootableBy } A \mathbb{Z} \Rightarrow \text{RootableBy } A \mathbb{N}$ via n ↦ n\in ℤ$$

Lean4

/-- A group is `ℕ`-rootable if it is `ℤ`-rootable
-/
@[to_additive /-- An additive group is `ℕ`-divisible if it `ℤ`-divisible. -/
    ]
def rootableByNatOfRootableByInt [RootableBy A ℤ] : RootableBy A ℕ
    where
  root a n := RootableBy.root a (n : ℤ)
  root_zero a := RootableBy.root_zero a
  root_cancel {n} a
    hn := by
    have := RootableBy.root_cancel a (show (n : ℤ) ≠ 0 from mod_cast hn)
    norm_num at this
    exact this

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