ext'

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

URI: https://scilib.ai/kg/mathlib#HomogeneousIdeal.ext'

English

If I and J agree on membership for every homogeneous element, then I = J.

Русский

Если принадлежности членов совпадают для всех однородных элементов, то I = J.

LaTeX

$$∀ I J, ∀ I, J, (∀ i, ∀ x ∈ 𝒜 i, x ∈ I ⇔ x ∈ J) ⇒ I = J$$

Lean4

theorem ext' {I J : HomogeneousIdeal 𝒜} (h : ∀ i, ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J) : I = J :=
  HomogeneousSubmodule.ext' 𝒜 𝒜 h

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

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

Разделы

Аффилиация

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