associatesEquivIsPrincipal_symm_apply

Mathlib.RingTheory.Ideal.IsPrincipal

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

← MathLib Explorer

English

The inverse of the equivalence sends a principal ideal back to its generator.

Русский

Обратное отображение эквивалентности возвращает генератор главного идеала.

LaTeX

$$symbolic_symm_apply(I) = generator(I)$$

Lean4

@[simp]
theorem associatesEquivIsPrincipal_symm_apply {I : Ideal R} (hI : IsPrincipal I) :
    (associatesEquivIsPrincipal R).symm ⟨I, hI⟩ = .mk hI.generator :=
  rfl

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

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

Разделы

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

Аффилиация

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