dual_ne_zero — Mathlib

English

The unit is contained in its trace-dual: 1 ≤ 1ᵛ.

Русский

Единица содержится в своей следовой дуальности: 1 ≤ 1ᵛ.

LaTeX

$$one_le_dual_one : 1 ≤ 1ᵛ.$$

Lean4

theorem dual_ne_zero (hI : I ≠ 0) : dual A K I ≠ 0 :=
  by
  obtain ⟨b, hb, hb'⟩ := I.prop
  suffices algebraMap B L b ∈ dual A K I by
    intro e
    rw [e, mem_zero_iff, ← (algebraMap B L).map_zero, (IsIntegralClosure.algebraMap_injective B A L).eq_iff] at this
    exact mem_nonZeroDivisors_iff_ne_zero.mp hb this
  rw [mem_dual hI]
  intro a ha
  apply IsIntegrallyClosed.isIntegral_iff.mp
  apply isIntegral_trace
  dsimp
  convert hb' a ha using 1
  · ext w
    exact IsIntegralClosure.isIntegral_iff (A := B)
  · exact (Algebra.smul_def _ _).symm

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