univ_eq_iUnion_smul — Mathlib

English

There is a natural embedding from the quotient by infimum of subgroups to the product of quotients by each subgroup.

Русский

Существует естественное вложение фактор-группы по инфимууму подгрупп в произведение фактор-групп по каждой подгруппе.

LaTeX

$$$H/ (\\bigwedge_i f_i).subgroupOf H \\hookrightarrow \\prod_i H/(f_i).subgroupOf H$$$

Lean4

/-- A group is made up of a disjoint union of cosets of a subgroup. -/
@[to_additive /-- An additive group is made up of a disjoint union of cosets of an additive
    subgroup. -/
    ]
theorem univ_eq_iUnion_smul (H : Subgroup α) : (Set.univ (α := α)) = ⋃ x : α ⧸ H, x.out • (H : Set _) :=
  by
  simp_rw [univ_eq_iUnion_orbit H.op, orbit_eq_out_smul]
  rfl

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