coe_dvd — Mathlib

English

Elements of the unit group divide any element of the monoid; i.e., ↑u divides a for any a.

Русский

Элементы группы единиц делят любой элемент моноида; то есть ↑u делит a для произвольного a.

LaTeX

$$$ \uparrow u \mid a $$$

Lean4

/-- Elements of the unit group of a monoid represented as elements of the monoid
divide any element of the monoid. -/
theorem coe_dvd : ↑u ∣ a :=
  ⟨↑u⁻¹ * a, by simp⟩

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