isSuccLimit_of_principal_mul — Mathlib

English

If o > 2 and o is principal for multiplication, then IsSuccLimit o.

Русский

Если o > 2 и o принципиален для умножения, то IsSuccLimit(o).

LaTeX

$$$(2 < o) \land Principal(\cdot * \cdot, o) \Rightarrow IsSuccLimit(o).$$$

Lean4

theorem isSuccLimit_of_principal_mul (ho₂ : 2 < o) (ho : Principal (· * ·) o) : IsSuccLimit o :=
  isSuccLimit_of_principal_add ((lt_succ 1).trans (succ_one ▸ ho₂)) (principal_add_of_principal_mul ho (ne_of_gt ho₂))

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