one_le_traceDual_one — Mathlib

English

Let I,J be submodules; then le statements and dual relations extend to sums: I ≤ (J · J')ᵛ ↔ I · J ≤ J'ᵛ.

Русский

Пусть I,J,J' — подмодули; тогда отношение неравенства сохраняется для сумм: I ≤ (J·J')ᵛ ↔ I·J ≤ (J')ᵛ.

LaTeX

$$$I \le (J J')^{\\vee} \iff I J \le (J')^{\\vee}.$$$

Lean4

theorem one_le_traceDual_one : (1 : Submodule B L) ≤ 1ᵛ :=
  by
  rw [le_traceDual_iff_map_le_one, mul_one, one_eq_range]
  rintro _ ⟨x, ⟨x, rfl⟩, rfl⟩
  rw [mem_one]
  apply IsIntegrallyClosed.isIntegral_iff.mp
  apply isIntegral_trace
  rw [IsIntegralClosure.isIntegral_iff (A := B)]
  exact ⟨_, rfl⟩

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