Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-07 07:05 faa7e52f

View on Github →

chore(group_theory/index): Add to_additive (#13191) This PR adds to_additive to the rest of group_theory/index.lean.

Estimated changes

Modified src/group_theory/coset.lean

Modified src/group_theory/index.lean

modified theorem subgroup.index_eq_one

modified theorem subgroup.index_inf_le

modified theorem subgroup.index_inf_ne_zero

modified theorem subgroup.index_ne_zero_of_fintype

modified theorem subgroup.inf_relindex_left

modified theorem subgroup.inf_relindex_right

modified theorem subgroup.relindex_dvd_of_le_left

modified theorem subgroup.relindex_eq_relindex_sup

modified theorem subgroup.relindex_inf_le

modified theorem subgroup.relindex_inf_ne_zero

modified theorem subgroup.relindex_le_of_le_left

modified theorem subgroup.relindex_le_of_le_right

modified theorem subgroup.relindex_mul_index

modified theorem subgroup.relindex_mul_relindex

modified theorem subgroup.relindex_ne_zero_trans