feat(group_theory/index): Intersection of finite index subgroups (#12776

)

This PR proves that if `H` and `K` are of finite index in `L`, then so is `H ⊓ K`.

src/group_theory/index.lean

@@ -209,6 +209,21 @@ lemma relindex_ne_zero_trans (hHK : H.relindex K ≠ 0) (hKL : K.relindex L ≠
 λ h, mul_ne_zero (mt (relindex_eq_zero_of_le_right (show K ⊓ L ≤ K, from inf_le_left)) hHK) hKL
   ((relindex_inf_mul_relindex H K L).trans (relindex_eq_zero_of_le_left inf_le_left h))
 
+lemma relindex_inf_ne_zero (hH : H.relindex L ≠ 0) (hK : K.relindex L ≠ 0) :
+  (H ⊓ K).relindex L ≠ 0 :=
+begin
+  replace hH : H.relindex (K ⊓ L) ≠ 0 := mt (relindex_eq_zero_of_le_right inf_le_right) hH,
+  rw ← inf_relindex_right at hH hK ⊢,
+  rw inf_assoc,
+  exact relindex_ne_zero_trans hH hK,
+end
+
+lemma index_inf_ne_zero (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0 :=
+begin
+  rw ← relindex_top_right at hH hK ⊢,
+  exact relindex_inf_ne_zero hH hK,
+end
+
 @[simp] lemma index_eq_one : H.index = 1 ↔ H = ⊤ :=
 ⟨λ h, quotient_group.subgroup_eq_top_of_subsingleton H (cardinal.to_nat_eq_one_iff_unique.mp h).1,
   λ h, (congr_arg index h).trans index_top⟩