ord_one

Mathlib.RingTheory.OrderOfVanishing

URI: https://scilib.ai/kg/mathlib#Ring.ord_one

← MathLib Explorer

English

The order of vanishing of the unit element is zero.

Русский

Порядок исчезновения единицы равен нулю.

LaTeX

$$ord_R(1) = 0$$

Lean4

/-- The order of vanishing of `1` is `0`.
-/
@[simp]
theorem ord_one : ord R 1 = 0 := by simp_all [ord, Ideal.span_singleton_one, Submodule.Quotient.subsingleton_iff]

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

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

Разделы

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

Аффилиация

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