instOne — Mathlib

English

There is a canonical unit element in the fractional ideals, provided by the top ideal, which acts as the identity for the relevant operation.

Русский

Существует канонический единичный элемент дробных идеалов, заданный верхним идеалом, который играет роль тождественного элемента для соответствующей операции.

LaTeX

$$$1 = \top \quad \text{in } \mathrm{FractionalIdeal}(S,P)$$$

Lean4

instance : One (FractionalIdeal S P) :=
  ⟨(⊤ : Ideal R)⟩

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