instOne

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

URI: https://scilib.ai/kg/mathlib#HomogeneousLocalization.instOne

English

There is a One instance for HomogeneousLocalization 𝒜 x, giving the identity element.

Русский

Существет инстанс единицы для HomogeneousLocalization 𝒜 x, обеспечивая тождественный элемент.

LaTeX

$$One on $\mathrm{HomogeneousLocalization}_{\mathcal{A}}(x)$$$

Lean4

instance : One (HomogeneousLocalization 𝒜 x) where one := Quotient.mk'' 1

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

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

Разделы

Аффилиация

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