English
Under the bot/top equivalence for base ideals, spanNorm distributes over product: spanNorm R (I J) = spanNorm R I · spanNorm R J.
Русский
При условии эквивалентности нижнего/верхнего для базовых идеалов, 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
/-- This condition `eq_bot_or_top` is equivalent to being a field.
However, `Ideal.spanNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R`
instance to a `Field R` instance. -/
theorem spanNorm_mul_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
spanNorm R (I * J) = spanNorm R I * spanNorm R J :=
by
refine le_antisymm ?_ (spanNorm_mul_spanNorm_le R _ _)
rcases eq_bot_or_top (spanNorm R I) with hI | hI
· rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]
exact bot_le
rw [hI, Ideal.top_mul]
rcases eq_bot_or_top (spanNorm R J) with hJ | hJ
· rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
rw [hJ]
exact le_top
