principal_mul_omega0 — Mathlib

English

Principal (· * ·) o is characterized by a condition involving left multiplication; in particular, it is equivalent to a bound condition on left-multiplication by elements less than o.

Русский

Принципиальность умножения слева для ординала o определяется условием, включающим слева умножение; в частности, эквивалентно ограничению на слева умножение на элементы меньше o.

LaTeX

$$$Principal(\cdot * \cdot, o) \iff (\text{условие равенства для левого умножения}).$$$

Lean4

theorem principal_mul_omega0 : Principal (· * ·) ω := fun a b ha hb =>
  match a, b, lt_omega0.1 ha, lt_omega0.1 hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
    dsimp only; rw [← natCast_mul]
    apply nat_lt_omega0

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