mk

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

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

← MathLib Explorer

English

The map mk is surjective onto HomogeneousLocalization 𝒜 x.

Русский

Карта mk сюръективна на HomogeneousLocalization 𝒜 x.

LaTeX

$$$\\text{Surjective}(\\mathrm{mk})$$$

Lean4

/-- Construct an element of `HomogeneousLocalization 𝒜 x` from a homogeneous fraction. -/
abbrev mk (y : HomogeneousLocalization.NumDenSameDeg 𝒜 x) : HomogeneousLocalization 𝒜 x :=
  Quotient.mk'' y

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

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

Разделы

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

Аффилиация

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