spanSingleton_mul_le_iff — Mathlib

English

Equality I = spanSingleton x * J is equivalent to a pair of conditions on elements and their images under multiplication by x.

Русский

Равенство I = spanSingleton x * J эквивалентно паре условий на элементы и их образ под умножением на x.

LaTeX

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

Lean4

theorem spanSingleton_mul_le_iff {x : P} {I J : FractionalIdeal S P} : spanSingleton _ x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J :=
  by
  simp only [mul_le, mem_spanSingleton]
  constructor
  · intro h zI hzI
    exact h x ⟨1, one_smul _ _⟩ zI hzI
  · rintro h _ ⟨z, rfl⟩ zI hzI
    rw [Algebra.smul_mul_assoc]
    exact Submodule.smul_mem J.1 _ (h zI hzI)

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