gcd_mul_addOrderOf_div_eq — Mathlib

English

For any m,n with 0 < n, we have gcd(m,n) · addOrderOf((m/n)p) = n.

Русский

Для любых m,n с 0 < n выполняется gcd(m,n) · addOrderOf((m/n)p) = n.

LaTeX

$$gcd$(m,n)$ · addOrderOf$\left(\left(\dfrac{m}{n}\right)p\right) = n$$

Lean4

theorem gcd_mul_addOrderOf_div_eq {n : ℕ} (m : ℕ) (hn : 0 < n) :
    m.gcd n * addOrderOf (↑(↑m / ↑n * p) : AddCircle p) = n :=
  by
  rw [natCast_div_mul_eq_nsmul, IsOfFinAddOrder.addOrderOf_nsmul]
  · rw [addOrderOf_period_div hn, Nat.gcd_comm, Nat.mul_div_cancel']
    exact n.gcd_dvd_left m
  · rwa [← addOrderOf_pos_iff, addOrderOf_period_div hn]

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