isComplement_subgroup_right_iff_existsUnique_quotientGroupMk

English

IsComplement S H is equivalent to the statement that for every q in G/H, there exists a unique s ∈ S with quotients equal: Quot.mk s = q.

Русский

IsComplement S H эквивалентно: для каждого q в G/H существует уникальный s ∈ S такой, что Quot.mk s = q.

LaTeX

$$$IsComplement S H \\\\Leftrightarrow \\\\forall q : G \\\\Div H, \\\\exists! s : S, QuotientGroup.mk s.1 = q$$$

Lean4

@[to_additive]
theorem isComplement_subgroup_right_iff_existsUnique_quotientGroupMk :
    IsComplement S H ↔ ∀ q : G ⧸ H, ∃! s : S, QuotientGroup.mk s.1 = q := by
  simp_rw [isComplement_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ← QuotientGroup.eq, QuotientGroup.forall_mk]

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