principal_add_of_principal_mul_opow

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 principal_add_of_principal_mul_opow (hb : 1 < b) (ho : Principal (· * ·) (b ^ o)) : Principal (· + ·) o :=
  by
  intro x y hx hy
  have := ho ((opow_lt_opow_iff_right hb).2 hx) ((opow_lt_opow_iff_right hb).2 hy)
  dsimp only at *
  rwa [← opow_add, opow_lt_opow_iff_right hb] at this

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