one_le_sum_inv_index_of_leftCoset_cover

English

If equality of subgroups holds, the quotient equivalence respects mk on representatives.

Русский

Если подгруппы равны, эквивалентность по фактор-группе сохраняет mk на представителей.

LaTeX

$$$\text{Subgroup.quotientEquivOfEq} h (\text{QuotientGroup.mk } a) = \text{QuotientGroup.mk } a$$$

Lean4

/-- Let the group `G` be the union of finitely many left cosets `g i • H i`. Then the
sum of the inverses of the indexes of the subgroups `H i` is greater than or equal to 1. -/
@[to_additive one_le_sum_inv_index_of_leftCoset_cover]
theorem one_le_sum_inv_index_of_leftCoset_cover : 1 ≤ ∑ i ∈ s, ((H i).index : ℚ)⁻¹ :=
  have := Classical.decPred (FiniteIndex : Subgroup G → Prop)
  (leftCoset_cover_filter_FiniteIndex_aux hcovers).2.1

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