split_dvd — Mathlib

English

If o is in normal form and split o = (o', m), then the ordinal corresponding to o' is a multiple of ω, i.e., ω divides repr(o').

Русский

Если o находится в нормальной форме и split o = (o', m), то соответствующая представлению o' оканчивается на кратное ω, то есть ω делит repr(o').

LaTeX

$$$\\forall o o' m\\,[NF\\ o]\\;\\big( split\\ o = (o', m) \\big) \\Rightarrow \\omega \\mid \\operatorname{repr} o'$$$

Lean4

theorem split_dvd {o o' m} [NF o] (h : split o = (o', m)) : ω ∣ repr o' :=
  by
  rcases e : split' o with ⟨a, n⟩
  rw [split_eq_scale_split' e] at h
  injection h; subst o'
  cases nf_repr_split' e; simp

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