leftRel_prod — Mathlib

English

The leftRel relation on a product s × s' is the product of the leftRel relations on s and s'.

Русский

Отношение leftRel на произведении s × s' равно произведению leftRel на s и на s'.

LaTeX

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

Lean4

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

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