principal_add_of_principal_mul — Mathlib

English

If o is principal for multiplication and o ≠ 2, then o is principal for addition as well.

Русский

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

LaTeX

$$$ Principal(\cdot * \cdot, o) \land o \neq 2 \Rightarrow Principal(\cdot + \cdot, o).$$$

Lean4

theorem principal_add_of_principal_mul (ho : Principal (· * ·) o) (ho₂ : o ≠ 2) : Principal (· + ·) o :=
  by
  rcases lt_or_gt_of_ne ho₂ with ho₁ | ho₂
  · replace ho₁ : o < succ 1 := by rwa [succ_one]
    rw [lt_succ_iff] at ho₁
    exact principal_add_of_le_one ho₁
  · refine fun a b hao hbo => lt_of_le_of_lt ?_ (ho (max_lt hao hbo) ho₂)
    dsimp only
    rw [← one_add_one_eq_two, mul_add, mul_one]
    exact add_le_add (le_max_left a b) (le_max_right a b)

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