principal_add_opow_of_principal_add

English

If a is principal for addition, then a^b is principal for addition for all b.

Русский

Если a является принципиальным для сложения, то a^b принципиален для сложения для любого b.

LaTeX

$$$Principal(\cdot + \cdot, a^b) \\forall b. $$$

Lean4

theorem principal_add_opow_of_principal_add {a} (ha : Principal (· + ·) a) (b : Ordinal) : Principal (· + ·) (a ^ b) :=
  by
  rcases principal_add_iff_zero_or_omega0_opow.1 ha with (rfl | ⟨c, rfl⟩)
  · rcases eq_or_ne b 0 with (rfl | hb)
    · rw [opow_zero]
      exact principal_add_one
    · rwa [zero_opow hb]
  · rw [← opow_mul]
    exact principal_add_omega0_opow _

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