const_add — Mathlib

English

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

Русский

Сумма двух константных секций есть константная секция с числителем f1 g2 + f2 g1 и знаменателем 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 g_2 + f_2 g_1) (g_1 g_2) U (\\lambda x hx => Submonoid.mul_mem _ (hu_1 x hx) (hu_2 x hx)) $$$

Lean4

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

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