dvd

Mathlib.Algebra.Divisibility.Units

URI: https://scilib.ai/kg/mathlib#IsUnit.dvd

← MathLib Explorer

English

Units divide any element: if u is a unit, then u | a for all a.

Русский

Единицы делят любой элемент: если u является единицей, то u | a для любого a.

LaTeX

$$$ (hu) : IsUnit u \rightarrow u \mid a $$$

Lean4

/-- Units of a monoid divide any element of the monoid. -/
@[simp]
theorem dvd (hu : IsUnit u) : u ∣ a := by
  rcases hu with ⟨u, rfl⟩
  apply Units.coe_dvd

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

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

Разделы

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

Аффилиация

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