From c3999605fb30977a49ac7edd949f9775cd291cdd Mon Sep 17 00:00:00 2001 From: newell Date: Mon, 2 Oct 2023 16:24:13 -0700 Subject: [PATCH] Fix/update main definitions documentation. --- Mathlib/GroupTheory/Index.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean index dac553b8dbe9e..042746dbf460f 100644 --- a/Mathlib/GroupTheory/Index.lean +++ b/Mathlib/GroupTheory/Index.lean @@ -27,7 +27,7 @@ Several theorems proved in this file are known as Lagrange's theorem. - `card_mul_index` : `Nat.card H * H.index = Nat.card G` - `index_mul_card` : `H.index * Fintype.card H = Fintype.card G` - `index_dvd_card` : `H.index ∣ Fintype.card G` -- `index_eq_mul_of_le` : If `H ≤ K`, then `H.index = K.index * (H.subgroupOf K).index` +- `relindex_mul_index` : If `H ≤ K`, then `H.relindex K * K.index = H.index` - `index_dvd_of_le` : If `H ≤ K`, then `K.index ∣ H.index` - `relindex_mul_relindex` : `relindex` is multiplicative in towers