isPrimal

Mathlib.Algebra.Divisibility.Units

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

English

Let u be a unit. Then u is primal.

Русский

Пусть u является единицей. Тогда u является прималом.

LaTeX

$$$$\operatorname{IsUnit}(u) \Rightarrow \operatorname{IsPrimal}(u).$$$$

Lean4

theorem isPrimal (hu : IsUnit u) : IsPrimal u := fun _ _ _ ↦ ⟨u, 1, hu.dvd, one_dvd _, (mul_one u).symm⟩

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

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

Разделы

Аффилиация

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