mul_def — Mathlib

English

The product I * J equals the fractional ideal whose underlying submodule is I * J and whose fractional property is the product of the fractional properties of I and J.

Русский

Произведение I * J равно дробному идеалу, основанному на подмодуле I * J и сохраняющему дробность через произведение свойств I и J.

LaTeX

$$I * J = ⟨I * J, I.isFractional.mul J.isFractional⟩$$

Lean4

theorem mul_def (I J : FractionalIdeal S P) : I * J = ⟨I * J, I.isFractional.mul J.isFractional⟩ := by
  simp only [← mul_eq_mul, mul_def']

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