addOrderOf_div_of_gcd_eq_one' — Mathlib

English

For any rational q, the order of (q·p) in AddCircle(p) equals the denominator of q.

Русский

Для любого рационального числа q порядок (q·p) в AddCircle(p) равен знаменателю q.

LaTeX

$$addOrderOf$(q\cdot p) = \operatorname{den}(q)$$$

Lean4

theorem addOrderOf_div_of_gcd_eq_one' {m : ℤ} {n : ℕ} (hn : 0 < n) (h : m.natAbs.gcd n = 1) :
    addOrderOf (↑(↑m / ↑n * p) : AddCircle p) = n := by
  cases m
  · simp only [Int.ofNat_eq_coe, Int.cast_natCast, Int.natAbs_natCast] at h ⊢
    exact addOrderOf_div_of_gcd_eq_one hn h
  · simp only [Int.cast_negSucc, neg_div, neg_mul, coe_neg, addOrderOf_neg]
    exact addOrderOf_div_of_gcd_eq_one hn h

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