Commit 2023-01-31 10:56 ae1428c0

View on Github →

feat: port GroupTheory.Coset (#1874) porting notes:

I had to add some really ugly type ascriptions so that whnf wouldn't time out. See Zulip
I opted for simp [mul_assoc] since we don't have the group tactic yet.
The library note at the end of the file should be updated.

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Coset.lean

added def LeftCosetEquivalence

added theorem QuotientGroup.card_quotient_rightRel

added theorem QuotientGroup.eq'

added theorem QuotientGroup.eq_class_eq_leftCoset

added theorem QuotientGroup.exists_mk

added theorem QuotientGroup.forall_mk

added theorem QuotientGroup.induction_on'

added theorem QuotientGroup.induction_on

added def QuotientGroup.leftRel

added theorem QuotientGroup.leftRel_apply

added theorem QuotientGroup.leftRel_eq

added theorem QuotientGroup.leftRel_r_eq_leftCosetEquivalence

added theorem QuotientGroup.mk_mul_of_mem

added theorem QuotientGroup.mk_out'_eq_mul

added theorem QuotientGroup.mk_surjective

added theorem QuotientGroup.out_eq'

added theorem QuotientGroup.preimage_image_mk

added def QuotientGroup.quotientRightRelEquivQuotientLeftRel

added theorem QuotientGroup.quotient_liftOn_mk

added def QuotientGroup.rightRel

added theorem QuotientGroup.rightRel_apply

added theorem QuotientGroup.rightRel_eq

added theorem QuotientGroup.rightRel_r_eq_rightCosetEquivalence

added def RightCosetEquivalence

added theorem Subgroup.card_comap_dvd_of_injective

added theorem Subgroup.card_dvd_of_injective

added theorem Subgroup.card_dvd_of_le

added theorem Subgroup.card_eq_card_quotient_mul_card_subgroup

added theorem Subgroup.card_quotient_dvd_card

added theorem Subgroup.card_subgroup_dvd_card

added def Subgroup.leftCosetEquivSubgroup

added def Subgroup.quotientEquivOfEq

added theorem Subgroup.quotientEquivOfEq_mk

added def Subgroup.quotientEquivProdOfLe'

added def Subgroup.quotientInfᵢEmbedding

added theorem Subgroup.quotientInfᵢEmbedding_apply_mk

added def Subgroup.quotientInfᵢSubgroupOfEmbedding

added theorem Subgroup.quotientInfᵢSubgroupOfEmbedding_apply_mk

added def Subgroup.quotientMapOfLe

added theorem Subgroup.quotientMapOfLe_apply_mk

added def Subgroup.quotientSubgroupOfEmbeddingOfLe

added theorem Subgroup.quotientSubgroupOfEmbeddingOfLe_apply_mk

added def Subgroup.quotientSubgroupOfMapOfLe

added theorem Subgroup.quotientSubgroupOfMapOfLe_apply_mk

added def Subgroup.rightCosetEquivSubgroup

added theorem eq_cosets_of_normal

added def leftCoset

added theorem leftCosetEquivalence_rel

added theorem leftCoset_assoc

added theorem leftCoset_eq_iff

added theorem leftCoset_mem_leftCoset

added theorem leftCoset_rightCoset

added theorem mem_leftCoset

added theorem mem_leftCoset_iff

added theorem mem_leftCoset_leftCoset

added theorem mem_own_leftCoset

added theorem mem_own_rightCoset

added theorem mem_rightCoset

added theorem mem_rightCoset_iff

added theorem mem_rightCoset_rightCoset

added theorem normal_iff_eq_cosets

added theorem normal_of_eq_cosets

added theorem one_leftCoset

added theorem orbit_subgroup_eq_rightCoset

added theorem orbit_subgroup_eq_self_of_mem

added theorem orbit_subgroup_one_eq_self

added def rightCoset

added theorem rightCosetEquivalence_rel

added theorem rightCoset_assoc

added theorem rightCoset_eq_iff

added theorem rightCoset_mem_rightCoset

added theorem rightCoset_one