Commit 2025-09-13 17:16 4e0206cb

View on Github →

chore(GroupTheory/Index): rename relindex to relIndex (#19872) Zulip discussion about renaming: [#PR reviews > #19872 rename relindex to relIndex @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2319872.20rename.20relindex.20to.20relIndex/near/515908054)

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Covolume.lean

added theorem ZLattice.covolume_div_covolume_eq_relIndex'

added theorem ZLattice.covolume_div_covolume_eq_relIndex

deleted theorem ZLattice.covolume_div_covolume_eq_relindex'

deleted theorem ZLattice.covolume_div_covolume_eq_relindex

Modified Mathlib/FieldTheory/Relrank.lean

Modified Mathlib/GroupTheory/Commensurable.lean

Modified Mathlib/GroupTheory/CosetCover.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

added theorem MulAction.IsBlock.ncard_block_eq_relIndex

deleted theorem MulAction.IsBlock.ncard_block_eq_relindex

Modified Mathlib/GroupTheory/Index.lean

added theorem AddSubgroup.relIndex_pointwise_smul

added theorem AddSubgroup.relIndex_toSubgroup

deleted theorem AddSubgroup.relindex_pointwise_smul

deleted theorem AddSubgroup.relindex_toSubgroup

added theorem Subgroup.exists_pow_mem_of_relIndex_ne_zero

deleted theorem Subgroup.exists_pow_mem_of_relindex_ne_zero

added theorem Subgroup.index_eq_zero_of_relIndex_eq_zero

deleted theorem Subgroup.index_eq_zero_of_relindex_eq_zero

added theorem Subgroup.inf_relIndex_left

added theorem Subgroup.inf_relIndex_right

deleted theorem Subgroup.inf_relindex_left

deleted theorem Subgroup.inf_relindex_right

added theorem Subgroup.pow_mem_of_relIndex_ne_zero_of_dvd

deleted theorem Subgroup.pow_mem_of_relindex_ne_zero_of_dvd

added theorem Subgroup.relIndex_bot_left

added theorem Subgroup.relIndex_bot_right

added theorem Subgroup.relIndex_comap

added theorem Subgroup.relIndex_comap_ne_zero

added theorem Subgroup.relIndex_dvd_card

added theorem Subgroup.relIndex_dvd_index_of_le

added theorem Subgroup.relIndex_dvd_index_of_normal

added theorem Subgroup.relIndex_dvd_of_le_left

added theorem Subgroup.relIndex_eq_one

added theorem Subgroup.relIndex_eq_zero_of_le_left

added theorem Subgroup.relIndex_eq_zero_of_le_right

added theorem Subgroup.relIndex_iInf_le

added theorem Subgroup.relIndex_iInf_ne_zero

added theorem Subgroup.relIndex_inf_le

added theorem Subgroup.relIndex_inf_mul_relIndex

added theorem Subgroup.relIndex_inf_ne_zero

added theorem Subgroup.relIndex_inter_ne_zero

added theorem Subgroup.relIndex_ker

added theorem Subgroup.relIndex_le_of_le_left

added theorem Subgroup.relIndex_le_of_le_right

added theorem Subgroup.relIndex_map_map

added theorem Subgroup.relIndex_map_map_of_injective

added theorem Subgroup.relIndex_mul_index

added theorem Subgroup.relIndex_mul_relIndex

added theorem Subgroup.relIndex_ne_zero

added theorem Subgroup.relIndex_ne_zero_trans

added theorem Subgroup.relIndex_pointwise_smul

added theorem Subgroup.relIndex_self

added theorem Subgroup.relIndex_subgroupOf

added theorem Subgroup.relIndex_sup_left

added theorem Subgroup.relIndex_sup_right

added theorem Subgroup.relIndex_toAddSubgroup

added theorem Subgroup.relIndex_top_left

added theorem Subgroup.relIndex_top_right

deleted theorem Subgroup.relindex_bot_left

deleted theorem Subgroup.relindex_bot_right

deleted theorem Subgroup.relindex_comap

deleted theorem Subgroup.relindex_comap_ne_zero

deleted theorem Subgroup.relindex_dvd_card

deleted theorem Subgroup.relindex_dvd_index_of_le

deleted theorem Subgroup.relindex_dvd_index_of_normal

deleted theorem Subgroup.relindex_dvd_of_le_left

deleted theorem Subgroup.relindex_eq_one

deleted theorem Subgroup.relindex_eq_zero_of_le_left

deleted theorem Subgroup.relindex_eq_zero_of_le_right

deleted theorem Subgroup.relindex_iInf_le

deleted theorem Subgroup.relindex_iInf_ne_zero

deleted theorem Subgroup.relindex_inf_le

deleted theorem Subgroup.relindex_inf_mul_relindex

deleted theorem Subgroup.relindex_inf_ne_zero

deleted theorem Subgroup.relindex_inter_ne_zero

deleted theorem Subgroup.relindex_ker

deleted theorem Subgroup.relindex_le_of_le_left

deleted theorem Subgroup.relindex_le_of_le_right

deleted theorem Subgroup.relindex_map_map

deleted theorem Subgroup.relindex_map_map_of_injective

deleted theorem Subgroup.relindex_mul_index

deleted theorem Subgroup.relindex_mul_relindex

deleted theorem Subgroup.relindex_ne_zero

deleted theorem Subgroup.relindex_ne_zero_trans

deleted theorem Subgroup.relindex_pointwise_smul

deleted theorem Subgroup.relindex_self

deleted theorem Subgroup.relindex_subgroupOf

deleted theorem Subgroup.relindex_sup_left

deleted theorem Subgroup.relindex_sup_right

deleted theorem Subgroup.relindex_toAddSubgroup

deleted theorem Subgroup.relindex_top_left

deleted theorem Subgroup.relindex_top_right

Modified Mathlib/GroupTheory/IndexNormal.lean

Modified Mathlib/GroupTheory/PGroup.lean

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/GroupTheory/Transfer.lean

Modified Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean

added theorem AddSubgroup.relIndex_eq_abs_det

added theorem AddSubgroup.relIndex_eq_natAbs_det

deleted theorem AddSubgroup.relindex_eq_abs_det

deleted theorem AddSubgroup.relindex_eq_natAbs_det

Modified Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

added theorem isCusp_iff_of_relIndex_ne_zero

deleted theorem isCusp_iff_of_relindex_ne_zero

Modified Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

Modified Mathlib/NumberTheory/NumberField/Units/Regulator.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Index.lean