le_dual_iff — Mathlib

English

The dual is zero if and only if the ideal is zero: dual A K I = 0 ⇔ I = 0.

Русский

Дуальность равна нулю тогда и только тогда, когда сам идеал равен нулю.

LaTeX

$$dual_eq_zero_iff : dual A K I = 0 ↔ I = 0.$$

Lean4

theorem le_dual_iff (hJ : J ≠ 0) : I ≤ dual A K J ↔ I * J ≤ dual A K 1 :=
  by
  by_cases hI : I = 0
  · simp [hI]
  rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual A K hJ, coe_dual_one, le_traceDual]

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