rightRel_prod — Mathlib

English

RightRel on the product s × s' is the product of RightRel on s and on s'.

Русский

RightRel на произведении s × s' равен произведению RightRel на s и на s'.

LaTeX

$$$\text{RightRel}(s \times s') = \text{RightRel}(s) \times \text{RightRel}(s')$$$

Lean4

@[to_additive rightRel_prod]
theorem rightRel_prod {β : Type*} [Group β] (s' : Subgroup β) :
    rightRel (s.prod s') = (rightRel s).prod (rightRel s') :=
  by
  refine Setoid.ext fun x y ↦ ?_
  rw [Setoid.prod_apply]
  simp_rw [rightRel_apply]
  rfl

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