_example

Mathlib.AlgebraicGeometry.AffineSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.AffineSpace._example

Lean4

/-- One should bear this equality in mind when breaking the `Spec R/ PrimeSpectrum R` abstraction
boundary, since these instances are not definitionally equal.
-/
example (R : CommRingCat) :
    inferInstance (α := Preorder (Spec R)) = inferInstance (α := Preorder (PrimeSpectrum R)ᵒᵈ) := by
  aesop (add simp spec_le_iff)

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

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

Разделы

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

Аффилиация

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