le_add_order_smul_norm_of_isOfFinAddOrder

English

If u has finite additive order and u ≠ 0, then p ≤ addOrderOf(u) · ‖u‖.

Русский

Если у имеет конечный порядок по сложению и не равен нулю, то p ≤ addOrderOf(u) · ‖u‖.

LaTeX

$$$\\text{If } u \\neq 0: \\; p \\le (\\operatorname{addOrderOf} u) \\cdot \\|u\\|$$$

Lean4

theorem le_add_order_smul_norm_of_isOfFinAddOrder {u : AddCircle p} (hu : IsOfFinAddOrder u) (hu' : u ≠ 0) :
    p ≤ addOrderOf u • ‖u‖ := by
  obtain ⟨n, hn⟩ := exists_norm_eq_of_isOfFinAddOrder hu
  replace hu : (addOrderOf u : ℝ) ≠ 0 := by
    norm_cast
    exact (addOrderOf_pos_iff.mpr hu).ne'
  conv_lhs => rw [← mul_one p]
  rw [hn, nsmul_eq_mul, ← mul_assoc, mul_comm _ p, mul_assoc, mul_div_cancel₀ _ hu, mul_le_mul_iff_right₀ hp.out,
    Nat.one_le_cast, Nat.one_le_iff_ne_zero]
  contrapose! hu'
  simpa only [hu', Nat.cast_zero, zero_div, mul_zero, norm_eq_zero] using hn

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