le_traceDual_mul_iff — Mathlib

English

For submodules I,J,J' of L over B, the trace-dual relation respects multiplication: I ≤ (J J')ᵛ if and only if I J ≤ J'ᵛ.

Русский

Для подмодулей I,J,J' множества L над B выполнено: I ≤ (J J')ᵛ тогда же, когда I J ≤ J'ᵛ.

LaTeX

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

Lean4

theorem le_traceDual_mul_iff {I J J' : Submodule B L} : I ≤ (J * J')ᵛ ↔ I * J ≤ J'ᵛ := by
  simp_rw [le_traceDual_iff_map_le_one, mul_assoc]

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