isUnit_den_zero

Mathlib.RingTheory.Localization.NumDen

URI: https://scilib.ai/kg/mathlib#IsFractionRing.isUnit_den_zero

English

den(0) is a unit; the prior result specialized to zero.

Русский

den(0) является единицей; повторение предыдущего результата для нуля.

LaTeX

$$$\\text{isUnit\_den\_zero}$$$

Lean4

theorem isUnit_den_zero : IsUnit (den A (0 : K) : A) := by simp [isUnit_den_iff, IsLocalization.isInteger_zero]

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

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

Разделы

Аффилиация

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