eq_spanSingleton_mul — Mathlib

English

A restatement of SpanSingleton multiplication equality via two-implications.

Русский

Переформулирование равенства умножения SpanSingleton через два импликации.

LaTeX

$$I = spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I$$

Lean4

theorem eq_spanSingleton_mul {x : P} {I J : FractionalIdeal S P} :
    I = spanSingleton _ x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I := by
  simp only [le_antisymm_iff, le_spanSingleton_mul_iff, spanSingleton_mul_le_iff]

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