coe_mul — Mathlib

English

For Ideals I,J of R, the fractional ideal obtained by coercing their product equals the product of the coerced ideals.

Русский

Для идеалов I,J кольца R дробный идеал, получаемый путём приведения их произведения, равен произведению их приводимых идеалов.

LaTeX

$$↑(I * J) = I * J$$

Lean4

@[simp, norm_cast]
theorem coe_mul (I J : FractionalIdeal S P) : (↑(I * J) : Submodule R P) = I * J := by simp only [mul_def, coe_mk]

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