iInf_mul — Mathlib

English

The infimum of a family of ideals, multiplied on the right by a fixed ideal I, equals the infimum of the products with I: (⨅ i, J_i) * I = ⨅ i, J_i * I.

Русский

И Infimum множества идеалов, умноженный справа на фиксированный идеал I, равен Infimum произведений: (⨅ i, J_i) * I = ⨅ i, J_i * I.

LaTeX

$$(⨅ i, J i) * I = ⨅ i, J i * I$$

Lean4

theorem iInf_mul (I : Ideal A) {ι : Type*} [Nonempty ι] (J : ι → Ideal A) : (⨅ i, J i) * I = ⨅ i, J i * I := by
  simp only [mul_iInf, mul_comm _ I]

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