Commit 2023-02-14 07:17 94fc5b20

View on Github →

feat: port GroupTheory.Index (#2222)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Parity.lean

Created Mathlib/GroupTheory/Index.lean

added theorem Subgroup.card_dvd_of_surjective

added theorem Subgroup.card_eq_one

added theorem Subgroup.card_mul_index

added theorem Subgroup.dvd_index_map

added theorem Subgroup.finiteIndex_of_finite_quotient

added theorem Subgroup.finiteIndex_of_le

added theorem Subgroup.index_bot

added theorem Subgroup.index_bot_eq_card

added theorem Subgroup.index_center_le_pow

added theorem Subgroup.index_comap

added theorem Subgroup.index_comap_of_surjective

added theorem Subgroup.index_dvd_card

added theorem Subgroup.index_dvd_of_le

added theorem Subgroup.index_eq_card

added theorem Subgroup.index_eq_one

added theorem Subgroup.index_eq_two_iff

added theorem Subgroup.index_eq_zero_of_relindex_eq_zero

added theorem Subgroup.index_inf_le

added theorem Subgroup.index_inf_ne_zero

added theorem Subgroup.index_infᵢ_le

added theorem Subgroup.index_infᵢ_ne_zero

added theorem Subgroup.index_ker

added theorem Subgroup.index_map

added theorem Subgroup.index_map_dvd

added theorem Subgroup.index_map_eq

added theorem Subgroup.index_mul_card

added theorem Subgroup.index_ne_zero_of_finite

added theorem Subgroup.index_top

added theorem Subgroup.inf_relindex_left

added theorem Subgroup.inf_relindex_right

added theorem Subgroup.mul_mem_iff_of_index_two

added theorem Subgroup.mul_self_mem_of_index_two

added theorem Subgroup.nat_card_dvd_of_injective

added theorem Subgroup.nat_card_dvd_of_le

added theorem Subgroup.nat_card_dvd_of_surjective

added theorem Subgroup.one_lt_index_of_ne_top

added theorem Subgroup.relindex_bot_left

added theorem Subgroup.relindex_bot_left_eq_card

added theorem Subgroup.relindex_bot_right

added theorem Subgroup.relindex_comap

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_inf_le

added theorem Subgroup.relindex_inf_mul_relindex

added theorem Subgroup.relindex_inf_ne_zero

added theorem Subgroup.relindex_infᵢ_le

added theorem Subgroup.relindex_infᵢ_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_mul_index

added theorem Subgroup.relindex_mul_relindex

added theorem Subgroup.relindex_ne_zero_trans

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_top_left

added theorem Subgroup.relindex_top_right

added theorem Subgroup.sq_mem_of_index_two

Modified Mathlib/Logic/Basic.lean