coe_injective

Mathlib.RingTheory.DividedPowers.Basic

URI: https://scilib.ai/kg/mathlib#DividedPowers.coe_injective

← MathLib Explorer

English

The map h ↦ h.dpow (as a function) is injective on DividedPowers I.

Русский

Отображение h ↦ h.dpow инъективно на DividedPowers I.

LaTeX

$$$$ \\text{DividedPowers.coe_injective} : \\mathrm{Injective}\\; (\\lambda h:\\mathrm{DividedPowers} I, h.dpow) $$$$

Lean4

theorem coe_injective : Function.Injective (fun (h : DividedPowers I) ↦ (h : ℕ → A → A)) := fun hI hI' h ↦
  by
  ext n x
  exact congr_fun (congr_fun h n) x

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

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

Разделы

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

Аффилиация

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