ofNat_isUnit

Mathlib.Algebra.Group.Int.Units

URI: https://scilib.ai/kg/mathlib#Int.ofNat_isUnit

English

The natural-number embedding preserves unit-ness: IsUnit(n) cast ↔ IsUnit(n).

Русский

Встраивание натурального числа сохраняет единицы: IsUnit(n.cast) ↔ IsUnit(n).

LaTeX

$$$ \operatorname{IsUnit}(n) \iff \operatorname{IsUnit}(n.{\text{cast}})$$$

Lean4

@[norm_cast]
theorem ofNat_isUnit {n : ℕ} : IsUnit (n : ℤ) ↔ IsUnit n := by simp [isUnit_iff_natAbs_eq]

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

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

Разделы

Аффилиация

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