mul_le_right_iff_opow_omega0_dvd

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.mul_le_right_iff_opow_omega0_dvd

← MathLib Explorer

English

ha > 0 implies a · b ≤ b iff a^ω divides b.

Русский

Если a > 0, тогда a · b ≤ b тогда и только если a^ω делит b.

LaTeX

$$$$ (a > 0) \Rightarrow a \cdot b \le b \iff (a^{\omega}) \mid b $$$$

Lean4

theorem mul_le_right_iff_opow_omega0_dvd {a b : Ordinal} (ha : 0 < a) : a * b ≤ b ↔ (a ^ ω) ∣ b :=
  by
  rw [← mul_eq_right_iff_opow_omega0_dvd]
  exact (isNormal_mul_right ha).le_iff_eq

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru