dual_ne_zero_iff

Mathlib.RingTheory.DedekindDomain.Different

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

English

For I ⊆ L and x ∈ L, x ∈ Iᵛ iff ∀ a ∈ I, IsIntegral A (traceForm K L x a).

Русский

Для I ⊆ L и x ∈ L: x ∈ Iᵛ тогда и только тогда, когда для всех a ∈ I выполняется IsIntegral A(traceForm x a).

LaTeX

$$mem_traceDual_iff_isIntegral : x ∈ I^∨ ↔ ∀ a ∈ I, IsIntegral A (traceForm K L x a).$$

Lean4

theorem dual_ne_zero_iff : dual A K I ≠ 0 ↔ I ≠ 0 :=
  dual_eq_zero_iff.not

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

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

Разделы

Аффилиация

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