instMulValueGroup — Mathlib

English

ValueGroup(A,K) is equipped with multiplication induced by representatives: (a1, a2) ↦ a1 a2 modulo the orbit relation.

Русский

ValueGroup(A,K) снабжается умножением, индуцированным по представителям: (a1,a2) ↦ a1 a2 по отношению орбит.

LaTeX

$$$\mathrm{Mul}(\mathrm{ValueGroup}(A,K))$ is defined by $\mathrm{Quotient}.mk''(a_1 a_2)$ whenever $x=\mathrm{Quotient}.mk'' a_1$ and $y=\mathrm{Quotient}.mk'' a_2$.$$

Lean4

instance : Mul (ValueGroup A K) :=
  Mul.mk fun x y =>
    Quotient.liftOn₂' x y (fun a b => Quotient.mk'' <| a * b)
      (by
        rintro _ _ a b ⟨c, rfl⟩ ⟨d, rfl⟩
        apply Quotient.sound'
        dsimp
        use c * d
        simp only [mul_smul, Algebra.smul_def, Units.smul_def]
        ring)

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