mk_mul_mk — Mathlib

English

The product of two localized elements is the localization of the product of numerators and denominators: mk a1 s1 · mk a2 s2 = mk (a1 a2) (s1 s2).

Русский

Произведение двух локализованных элементов равно локализации произведения числителей и знаменателей: mk(a1,s1) · mk(a2,s2) = mk(a1 a2, s1 s2).

LaTeX

$$$\\mathrm{mk}(a_1,s_1) \\cdot \\mathrm{mk}(a_2,s_2) = \\mathrm{mk}(a_1 a_2, s_1 s_2)$$$

Lean4

theorem mk_mul_mk {A : Type*} [Semiring A] [Algebra R A] {a₁ a₂ : A} {s₁ s₂ : S} :
    mk a₁ s₁ * mk a₂ s₂ = mk (a₁ * a₂) (s₁ * s₂) :=
  rfl

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