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