addOrderOf_coe_eq_zero_iff_forall_rat_ne_div

English

The number of elements of AddCircle(p) with a fixed finite order n is φ(n), i.e., the set {u ∈ AddCircle(p) | addOrderOf(u) = n} has cardinal φ(n).

Русский

Число точек AddCircle(p) имеющих конечный порядок n равно φ(n).

LaTeX

$$Nat.card{u: AddCircle(p) // addOrderOf(u) = n} = φ(n)$$

Lean4

@[deprecated not_isOfFinAddOrder_iff_forall_rat_ne_div (since := "2025-08-13")]
theorem addOrderOf_coe_eq_zero_iff_forall_rat_ne_div {a : 𝕜} :
    addOrderOf (a : AddCircle p) = 0 ↔ ∀ q : ℚ, (q : 𝕜) ≠ a / p := by simp [not_isOfFinAddOrder_iff_forall_rat_ne_div]

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