mono — Mathlib

English

IsOfFinOrder x and y in a Monoid G imply IsOfFinOrder y when orderOf y divides orderOf x.

Русский

Пусть x, y ∈ моноид G; если IsOfFinOrder x и orderOf y делит orderOf x, то IsOfFinOrder y.

LaTeX

$$IsOfFinOrder x \\Rightarrow (orderOf y \\mid orderOf x) \\Rightarrow IsOfFinOrder y$$

Lean4

@[to_additive]
theorem mono [Monoid β] {y : β} (hx : IsOfFinOrder x) (h : orderOf y ∣ orderOf x) : IsOfFinOrder y := by
  rw [← orderOf_pos_iff] at hx ⊢; exact Nat.pos_of_dvd_of_pos h hx

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