extended_zero

Mathlib.RingTheory.FractionalIdeal.Extended

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.extended_zero

← MathLib Explorer

English

The extended image of 0 is 0.

Русский

Расширение нуля даёт нуль.

LaTeX

$$$\text{extended } L hf(0) = 0$$$

Lean4

@[simp]
theorem extended_zero : extended L hf (0 : FractionalIdeal M K) = 0 :=
  have : ((0 : FractionalIdeal M K) : Set K) = {0} := by ext; simp
  coeToSubmodule_injective (by simp [this])

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

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

Разделы

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

Аффилиация

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