le_spanSingleton_mul_iff — Mathlib

English

Characterizes when an inclusion holds between a fractional ideal and spanSingleton x times another fractional ideal.

Русский

Характеризует условие включения между дробным идеалом и произведением spanSingleton и другим дробным идеалом.

LaTeX

$$I ≤ spanSingleton S x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI$$

Lean4

theorem le_spanSingleton_mul_iff {x : P} {I J : FractionalIdeal S P} :
    I ≤ spanSingleton S x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI :=
  show (∀ {zI} (_ : zI ∈ I), zI ∈ spanSingleton _ x * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI by
    simp only [mem_singleton_mul, eq_comm]

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