spanNorm_mul_spanNorm_le — Mathlib

English

If eq_bot_or_top holds for ideals of the base ring R, then spanNorm respects multiplication consistently: spanNorm(R, I J) = spanNorm(R, I) spanNorm(R, J).

Русский

Если выполняется eq_bot_or_top для идеалов R, то spanNorm сохраняет умножение: spanNorm(R, I J) = spanNorm(R, I) spanNorm(R, J).

LaTeX

$$$$\forall I,J,\; \operatorname{spanNorm}(R,I J) = \operatorname{spanNorm}(R,I) \cdot \operatorname{spanNorm}(R,J). $$$$

Lean4

theorem spanNorm_mul_spanNorm_le (I J : Ideal S) : spanNorm R I * spanNorm R J ≤ spanNorm R (I * J) :=
  by
  rw [spanNorm, spanNorm, spanNorm]
  nth_rw 1 [map]; nth_rw 1 [map]
  rw [Ideal.span_mul_span', ← Set.image_mul]
  refine Ideal.span_mono (Set.monotone_image ?_)
  rintro _ ⟨x, hxI, y, hyJ, rfl⟩
  exact Ideal.mul_mem_mul hxI hyJ

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