addOrderOf_coe_rat — Mathlib

English

Same fact as above expressed for Rat, i.e., the order of (q·p) in AddCircle(p) is the denominator of q.

Русский

То же самое для рациона Rat: порядок (q·p) в AddCircle(p) равен знаменателю q.

LaTeX

$$addOrderOf$(q\cdot p) = \den(q)$$

Lean4

theorem addOrderOf_coe_rat {q : ℚ} : addOrderOf (↑(↑q * p) : AddCircle p) = q.den :=
  by
  have : (↑(q.den : ℤ) : 𝕜) ≠ 0 := by
    norm_cast
    exact q.pos.ne.symm
  rw [← q.num_divInt_den, Rat.cast_divInt_of_ne_zero _ this, Int.cast_natCast, Rat.num_divInt_den,
    addOrderOf_div_of_gcd_eq_one' q.pos q.reduced]

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