instMul — Mathlib

English

The multiplication on HomogeneousLocalization 𝒜 x is given by lifting to representatives and multiplying them, then passing to the quotient.

Русский

Умножение на HomogeneousLocalization 𝒜 x задаётся возведением представителя в произведение и переходом к эквивалентости по фактору.

LaTeX

$$Mul on $\mathrm{HomogeneousLocalization}_{\mathcal{A}}(x)$ is defined via representatives.$$

Lean4

instance : Mul (HomogeneousLocalization 𝒜 x) where
  mul :=
    Quotient.map₂ (· * ·)
      fun c1 c2 (h : Localization.mk _ _ = Localization.mk _ _) c3 c4
        (h' : Localization.mk _ _ = Localization.mk _ _) =>
      by
      change Localization.mk _ _ = Localization.mk _ _
      simp only [num_mul, den_mul]
      convert congr_arg₂ (· * ·) h h' <;> rw [Localization.mk_mul] <;> rfl

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