English
If H' ≤ H, there exists a left transversal S inside H with SH' = H and |S|·|H'| = |H|.
Русский
Если H' ⊆ H, то внутри H существует левая трансверсаль S с SH' = H и |S|·|H'| = |H|.
LaTeX
$$There exists S with S * H' = H and Nat.card S * Nat.card H' = Nat.card H.$$
Lean4
/-- Given two subgroups `H' ⊆ H`, there exists a left transversal to `H'` inside `H`. -/
@[to_additive /-- Given two subgroups `H' ⊆ H`, there exists a transversal to `H'` inside `H` -/
]
theorem exists_left_transversal_of_le {H' H : Subgroup G} (h : H' ≤ H) :
∃ S : Set G, S * H' = H ∧ Nat.card S * Nat.card H' = Nat.card H :=
by
let H'' : Subgroup H := H'.comap H.subtype
have : H' = H''.map H.subtype := by simp [H'', h]
rw [this]
obtain ⟨S, cmem, -⟩ := H''.exists_isComplement_left 1
refine ⟨H.subtype '' S, ?_, ?_⟩
· have : H.subtype '' (S * H'') = H.subtype '' S * H''.map H.subtype := image_mul H.subtype
rw [← this, cmem.mul_eq]
simp
· rw [← cmem.card_mul_card]
refine congr_arg₂ (· * ·) ?_ ?_ <;> exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm
