const_mul — Mathlib

English

The product of two constant sections is a constant section with numerator f1 f2 and denominator g1 g2.

Русский

Произведение двух константных секций есть константная секция с числителем f1 f2 и знаменателем g1 g2.

LaTeX

$$$ const_R f_1 g_1 U hu_1 * const_R f_2 g_2 U hu_2 = const_R (f_1 f_2) (g_1 g_2) U (\\lambda x hx => Submonoid.mul_mem _ (hu_1 x hx) (hu_2 x hx)) $$$

Lean4

theorem const_mul (f₁ f₂ g₁ g₂ : R) (U hu₁ hu₂) :
    const R f₁ g₁ U hu₁ * const R f₂ g₂ U hu₂ =
      const R (f₁ * f₂) (g₁ * g₂) U fun x hx => Submonoid.mul_mem _ (hu₁ x hx) (hu₂ x hx) :=
  Subtype.eq <| funext fun x => Eq.symm <| IsLocalization.mk'_mul _ f₁ f₂ ⟨g₁, hu₁ x x.2⟩ ⟨g₂, hu₂ x x.2⟩

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