mul — Mathlib

English

If I and J are homogeneous ideals, then their product I · J is homogeneous.

Русский

Если I и J — однородные идеалы, то их произведение I · J также однородно.

LaTeX

$$$ (I J) \text{ is homogeneous } \Rightarrow (I * J) \text{ is homogeneous} $$$

Lean4

theorem mul {I J : Ideal A} (HI : I.IsHomogeneous 𝒜) (HJ : J.IsHomogeneous 𝒜) : (I * J).IsHomogeneous 𝒜 :=
  by
  rw [Ideal.IsHomogeneous.iff_exists] at HI HJ ⊢
  obtain ⟨⟨s₁, rfl⟩, ⟨s₂, rfl⟩⟩ := HI, HJ
  rw [Ideal.span_mul_span']
  exact ⟨s₁ * s₂, congr_arg _ <| (Set.image_mul (homogeneousSubmonoid 𝒜).subtype).symm⟩

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