rootableByIntOfRootableByNat — Mathlib

English

If A is a group and is ℕ-rootable, then it is ℤ-rootable.

Русский

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

LaTeX

$$$\text{RootableBy } A \mathbb{N} \Rightarrow \text{RootableBy } A \mathbb{Z}$$$

Lean4

/-- A group is `ℤ`-rootable if it is `ℕ`-rootable.
-/
@[to_additive /-- An additive group is `ℤ`-divisible if it is `ℕ`-divisible. -/
    ]
def rootableByIntOfRootableByNat [RootableBy A ℕ] : RootableBy A ℤ
    where
  root a
    z :=
    match z with
    | (n : ℕ) => RootableBy.root a n
    | -[n+1] => (RootableBy.root a (n + 1))⁻¹
  root_zero a := RootableBy.root_zero a
  root_cancel {n} a
    hn := by
    cases n
    · rw [Int.ofNat_eq_coe, Nat.cast_ne_zero] at hn
      simp [RootableBy.root_cancel _ hn]
    · simp [RootableBy.root_cancel _ (Nat.add_one_ne_zero _)]

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