associatesEquivIsPrincipal_map_one

Mathlib.RingTheory.Ideal.IsPrincipal

URI: https://scilib.ai/kg/mathlib#Ideal.associatesEquivIsPrincipal_map_one

← MathLib Explorer

English

The image of the unit under the equivalence is the unit ideal.

Русский

Образ единицы при эквивалентности — это единичный идеал.

LaTeX

$$$(associatesEquivIsPrincipal \; R\; 1) = 1$$$

Lean4

@[simp]
theorem associatesEquivIsPrincipal_map_one : (associatesEquivIsPrincipal R 1 : Ideal R) = 1 := by
  rw [one_eq_mk_one, associatesEquivIsPrincipal_apply, span_singleton_one, one_eq_top]

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

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

Разделы

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

Аффилиация

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