awayMapₐ_apply

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

URI: https://scilib.ai/kg/mathlib#HomogeneousLocalization.awayMapₐ_apply

English

The mk construction is surjective onto Away, up to the grading data.

Русский

Конструкция mk сюръективна на Away с учётом градации.

LaTeX

$$$$ \text{protected theorem mk_surjective}\; {d} \; (hf : f ∈ 𝒜 d) (x : Away 𝒜 f) : ∃ n a ha, Away.mk 𝒜 hf n a ha = x. $$$$

Lean4

@[simp]
theorem awayMapₐ_apply (a) : awayMapₐ 𝒜 hg hx a = awayMap 𝒜 hg hx a :=
  rfl

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

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

Разделы

Аффилиация

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