eq_zero_or_opow_omega0_le_of_mul_eq_right

English

a · b = b iff a^ω divides b.

Русский

a · b = b эквивалентно тому, что a^ω делит b.

LaTeX

$$$$ a \cdot b = b \iff (a^{\omega}) \mid b $$$$

Lean4

theorem eq_zero_or_opow_omega0_le_of_mul_eq_right {a b : Ordinal} (hab : a * b = b) : b = 0 ∨ a ^ ω ≤ b :=
  by
  rcases eq_zero_or_pos a with ha | ha
  · rw [ha, zero_opow omega0_ne_zero]
    exact Or.inr (Ordinal.zero_le b)
  rw [or_iff_not_imp_left]
  intro hb
  rw [← nfp_mul_one ha]
  rw [← Ne, ← one_le_iff_ne_zero] at hb
  exact nfp_le_fp (isNormal_mul_right ha).monotone hb (le_of_eq hab)

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